# HG changeset patch # User wenzelm # Date 1676284546 -3600 # Node ID c7d893278aec7dea66a7a97a9cb5a28a31b839ff # Parent e9f1fcb9b358b7be1fea7d9401fbd179b2475c2f proper synchronized access to mutable state, to support concurrency eventually; diff -r e9f1fcb9b358 -r c7d893278aec src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Mon Feb 13 11:25:01 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Mon Feb 13 11:35:46 2023 +0100 @@ -174,18 +174,20 @@ private var _running = Map.empty[String, Build_Job] private var _results = Map.empty[String, Build_Process.Result] - private def remove_pending(name: String): Unit = { + private def remove_pending(name: String): Unit = synchronized { _build_graph = _build_graph.del_node(name) _build_order = _build_order - name } - private def next_pending(): Option[String] = + private def next_pending(): Option[String] = synchronized { _build_order.iterator .dropWhile(name => _running.isDefinedAt(name) || !_build_graph.is_minimal(name)) .nextOption() + } - private def used_node(i: Int): Boolean = + private def used_node(i: Int): Boolean = synchronized { _running.valuesIterator.exists(job => job.numa_node.isDefined && job.numa_node.get == i) + } private def session_finished(session_name: String, process_result: Process_Result): String = "Finished " + session_name + " (" + process_result.timing.message_resources + ")" @@ -250,9 +252,11 @@ if (!process_result.interrupted) progress.echo(process_result_tail.out) } - remove_pending(session_name) - _running -= session_name - _results += (session_name -> Build_Process.Result(false, output_heap, process_result_tail)) + synchronized { + remove_pending(session_name) + _running -= session_name + _results += (session_name -> Build_Process.Result(false, output_heap, process_result_tail)) + } } private def start_job(session_name: String): Unit = { @@ -288,13 +292,17 @@ val all_current = current && ancestor_results.forall(_.current) if (all_current) { - remove_pending(session_name) - _results += (session_name -> Build_Process.Result(true, output_heap, Process_Result.ok)) + synchronized { + remove_pending(session_name) + _results += (session_name -> Build_Process.Result(true, output_heap, Process_Result.ok)) + } } else if (no_build) { progress.echo_if(verbose, "Skipping " + session_name + " ...") - remove_pending(session_name) - _results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.error)) + synchronized { + remove_pending(session_name) + _results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.error)) + } } else if (ancestor_results.forall(_.ok) && !progress.stopped) { progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...") @@ -308,16 +316,20 @@ new Resources(session_background, log = log, command_timings = build_context(session_name).old_command_timings) - val numa_node = _numa_nodes.next(used_node) - val job = - new Build_Job(progress, session_background, store, do_store, - resources, session_setup, input_heaps, numa_node) - _running += (session_name -> job) + synchronized { + val numa_node = _numa_nodes.next(used_node) + val job = + new Build_Job(progress, session_background, store, do_store, + resources, session_setup, input_heaps, numa_node) + _running += (session_name -> job) + } } else { progress.echo(session_name + " CANCELLED") - remove_pending(session_name) - _results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.undefined)) + synchronized { + remove_pending(session_name) + _results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.undefined)) + } } } @@ -327,12 +339,12 @@ } def run(): Map[String, Build_Process.Result] = { - while (!_build_graph.is_empty) { - if (progress.stopped) _running.valuesIterator.foreach(_.terminate()) + while (synchronized { !_build_graph.is_empty }) { + if (progress.stopped) synchronized { _running.valuesIterator.foreach(_.terminate()) } - _running.find({ case (_, job) => job.is_finished }) match { + synchronized { _running } .find({ case (_, job) => job.is_finished }) match { case Some((session_name, job)) => finish_job(session_name, job) - case None if _running.size < (max_jobs max 1) => + case None if synchronized { _running.size } < (max_jobs max 1) => next_pending() match { case Some(session_name) => start_job(session_name) case None => sleep() @@ -341,6 +353,6 @@ } } - _results + synchronized { _results } } }