explicit shutdown of scheduler and worker thread farm, assuming Session.shutdown() before saving heap image;
authorwenzelm
Sat, 10 Jan 2015 14:28:41 +0100
changeset 59340 734bb148503e
parent 59339 abc53a03ca1c
child 59341 a74eb8e0907a
explicit shutdown of scheduler and worker thread farm, assuming Session.shutdown() before saving heap image; discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage;
src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Jan 10 13:02:27 2015 +0100
+++ b/src/Pure/Concurrent/future.ML	Sat Jan 10 14:28:41 2015 +0100
@@ -302,7 +302,9 @@
     val max_active0 = ! max_active;
     val max_workers0 = ! max_workers;
 
-    val m = if ! do_shutdown then 0 else Multithreading.max_threads_value ();
+    val m =
+      if ! do_shutdown andalso Task_Queue.all_passive (! queue) then 0
+      else Multithreading.max_threads_value ();
     val _ = max_active := m;
     val _ = max_workers := 2 * m;
 
@@ -336,7 +338,6 @@
 
     (* shutdown *)
 
-    val _ = if Task_Queue.all_passive (! queue) then do_shutdown := true else ();
     val continue = not (! do_shutdown andalso null (! workers));
     val _ = if continue then () else (report_status (); scheduler := NONE);
 
@@ -657,7 +658,8 @@
   else
     SYNCHRONIZED "shutdown" (fn () =>
       while scheduler_active () do
-       (Multithreading.tracing 1 (fn () => "SHUTDOWN: wait");
+       (do_shutdown := true;
+        Multithreading.tracing 1 (fn () => "SHUTDOWN: wait");
         wait scheduler_event));