# HG changeset patch
# User wenzelm
# Date 1676986207 -3600
# Node ID db479840d6add9551fcba5ca3dd4eb994fb57326
# Parent  35c1e34fc693c9a1ac5c622f9e2271b1b37fd56b
clarified signature;

diff -r 35c1e34fc693 -r db479840d6ad src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Feb 21 13:02:33 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Feb 21 14:30:07 2023 +0100
@@ -172,8 +172,17 @@
     running: Map[String, Build_Job] = Map.empty,
     results: Map[String, Build_Process.Result] = Map.empty
   ) {
-    def get_numa: (Int, Set[Int]) = (numa_index, numa_running)
-    def put_numa(i: Int): State = copy(numa_index = i)
+    def numa_next(numa_nodes: List[Int]): (Option[Int], State) =
+      if (numa_nodes.isEmpty) (None, this)
+      else {
+        val available = numa_nodes.zipWithIndex
+        val used = Set.from(for (job <- running.valuesIterator; i <- job.numa_node) yield i)
+        val candidates = available.drop(numa_index) ::: available.take(numa_index)
+        val (n, i) =
+          candidates.find({ case (n, i) => i == numa_index && !used(n) }) orElse
+          candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head
+        (Some(n), copy(numa_index = (i + 1) % available.length))
+      }
 
     def finished: Boolean = pending.isEmpty
 
@@ -183,9 +192,6 @@
 
     def is_running(name: String): Boolean = running.isDefinedAt(name)
 
-    def numa_running: Set[Int] =
-      Set.from(for (job <- running.valuesIterator; i <- job.numa_node) yield i)
-
     def stop_running(): Unit = running.valuesIterator.foreach(_.terminate())
 
     def finished_running(): List[Build_Job.Build_Session] =
@@ -262,31 +268,12 @@
     else None
   }
 
-  protected def next_numa_node(): Option[Int] = synchronized {
-    val available = build_context.numa_nodes.zipWithIndex
-    if (available.isEmpty) None
-    else {
-      val (index, used) = _state.get_numa
-      val candidates = available.drop(index) ::: available.take(index)
-      val (n, i) =
-        candidates.find({ case (n, i) => i == index && !used(n) }) orElse
-        candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head
-      _state = _state.put_numa((i + 1) % available.length)
-      Some(n)
-    }
-  }
-
   protected def stop_running(): Unit = synchronized { _state.stop_running() }
 
   protected def finished_running(): List[Build_Job.Build_Session] = synchronized {
     _state.finished_running()
   }
 
-  protected def job_running(name: String, job: Build_Job): Build_Job = synchronized {
-    _state = _state.add_running(name, job)
-    job
-  }
-
   protected def finish_job(job: Build_Job.Build_Session): Unit = {
     val session_name = job.session_name
     val process_result = job.join
@@ -407,10 +394,12 @@
 
       val job =
         synchronized {
-          val numa_node = next_numa_node()
-          job_running(session_name,
+          val (numa_node, state1) = _state.numa_next(build_context.numa_nodes)
+          val job =
             new Build_Job.Build_Session(progress, session_background, store, do_store,
-              resources, build_context.session_setup, input_heaps, numa_node))
+              resources, build_context.session_setup, input_heaps, numa_node)
+          _state = state1.add_running(session_name, job)
+          job
         }
       job.start()
     }