# HG changeset patch
# User wenzelm
# Date 1677704809 -3600
# Node ID e27bc79572978bb1715db65260febde28946a100
# Parent  94dcf2c3895a41efbdad5f5264f5fa69f6b831f3
more robust: proper synchronization of transition from next_job to start_session;

diff -r 94dcf2c3895a -r e27bc7957297 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 21:53:12 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 22:06:49 2023 +0100
@@ -556,10 +556,9 @@
     }
     else None
 
-  protected def start_session(session_name: String): Unit = {
-    val ancestor_results = synchronized_database {
-      _state.get_results(build_context.sessions(session_name).ancestors)
-    }
+  protected def start_session(state: Build_Process.State, session_name: String): Build_Process.State = {
+    val ancestor_results = state.get_results(build_context.sessions(session_name).ancestors)
+
     val input_shasum =
       if (ancestor_results.isEmpty) {
         SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
@@ -589,27 +588,21 @@
     val all_current = current && ancestor_results.forall(_.current)
 
     if (all_current) {
-      synchronized_database {
-        _state = _state.
-          remove_pending(session_name).
-          make_result(session_name, Process_Result.ok, output_shasum, current = true)
-      }
+      state
+        .remove_pending(session_name)
+        .make_result(session_name, Process_Result.ok, output_shasum, current = true)
     }
     else if (build_context.no_build) {
       progress.echo_if(verbose, "Skipping " + session_name + " ...")
-      synchronized_database {
-        _state = _state.
-          remove_pending(session_name).
-          make_result(session_name, Process_Result.error, output_shasum)
-      }
+      state.
+        remove_pending(session_name).
+        make_result(session_name, Process_Result.error, output_shasum)
     }
     else if (!ancestor_results.forall(_.ok) || progress.stopped) {
       progress.echo(session_name + " CANCELLED")
-      synchronized_database {
-        _state = _state.
-          remove_pending(session_name).
-          make_result(session_name, Process_Result.undefined, output_shasum)
-      }
+      state
+        .remove_pending(session_name)
+        .make_result(session_name, Process_Result.undefined, output_shasum)
     }
     else {
       progress.echo((if (store_heap) "Building " else "Running ") + session_name + " ...")
@@ -629,15 +622,12 @@
         new Resources(session_background, log = log,
           command_timings = build_context.old_command_timings(session_name))
 
-      synchronized_database {
-        val (numa_node, state1) = _state.numa_next(build_context.numa_nodes)
-        val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
-        val job =
-          new Build_Job.Session_Job(build_context, session_background, session_heaps,
-            store_heap, resources, input_shasum, node_info)
-        _state = state1.add_running(session_name, job)
-        job
-      }
+      val (numa_node, state1) = state.numa_next(build_context.numa_nodes)
+      val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
+      val job =
+        new Build_Job.Session_Job(build_context, session_background, session_heaps,
+          store_heap, resources, input_shasum, node_info)
+      state1.add_running(session_name, job)
     }
   }
 
@@ -652,6 +642,18 @@
         build_options.seconds("editor_input_delay").sleep()
       }
 
+    def start(): Boolean = synchronized_database {
+      next_job(_state) match {
+        case Some(name) =>
+          if (Build_Job.is_session_name(name)) {
+            _state = start_session(_state, name)
+            true
+          }
+          else error("Unsupported build job name " + quote(name))
+        case None => false
+      }
+    }
+
     if (finished()) {
       progress.echo_warning("Nothing to build")
       Map.empty[String, Process_Result]
@@ -672,15 +674,12 @@
           }
         }
 
-        synchronized_database { next_job(_state) } match {
-          case Some(name) =>
-            if (Build_Job.is_session_name(name)) start_session(name)
-            else error("Unsupported build job name " + quote(name))
-          case None =>
-            sync_database()
-            sleep()
+        if (!start()) {
+          sync_database()
+          sleep()
         }
       }
+
       synchronized_database {
         for ((name, result) <- _state.results) yield name -> result.process_result
       }