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;
--- 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));