# HG changeset patch
# User desharna
# Date 1710700234 -3600
# Node ID 6fc9c4344df428fe69c172e2889cf7459feded58
# Parent  caa9dbffd712e7d6f75e9ead07f242bf67cf5863# Parent  1966578feff8bc95d99e12db093bcdb6c7435820
merged

diff -r caa9dbffd712 -r 6fc9c4344df4 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Sun Mar 17 12:34:11 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sun Mar 17 19:30:34 2024 +0100
@@ -568,13 +568,26 @@
       if (is_empty) true
       else elapsed() > options.seconds("build_schedule_outdated_delay")
 
-    def next(hostname: String, state: Build_Process.State): List[String] =
-      for {
-        task <- state.next_ready
-        node = graph.get_node(task.name)
-        if hostname == node.node_info.hostname
-        if graph.imm_preds(node.job_name).subsetOf(state.results.keySet)
-      } yield task.name
+    def next(hostname: String, state: Build_Process.State): List[String] = {
+      val next_nodes =
+        for {
+          task <- state.next_ready
+          node = graph.get_node(task.name)
+          if hostname == node.node_info.hostname
+        } yield node
+
+      val (ready, waiting) =
+        next_nodes.partition(node => graph.imm_preds(node.job_name).subsetOf(state.results.keySet))
+      val running = state.running.values.toList.map(_.node_info).filter(_.hostname == hostname)
+
+      def try_run(ready: List[Schedule.Node], next: Schedule.Node): List[Schedule.Node] = {
+        val existing = ready.map(_.node_info) ::: running
+        val is_distinct = existing.forall(_.rel_cpus.intersect(next.node_info.rel_cpus).isEmpty)
+        if (existing.forall(_.rel_cpus.nonEmpty) && is_distinct) next :: ready else ready
+      }
+
+      waiting.foldLeft(ready)(try_run).map(_.job_name)
+    }
 
     def exists_next(hostname: String, state: Build_Process.State): Boolean =
       next(hostname, state).nonEmpty