immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
authorwenzelm
Sat, 13 Aug 2011 00:34:54 +0200
changeset 44173 aaaa13e297dc
parent 44172 21f97048b478
child 44175 28cdf93076f4
immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029); more careful treatment of last_round on startup/shutdown;
src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri Aug 12 23:29:28 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Aug 13 00:34:54 2011 +0200
@@ -310,7 +310,7 @@
     val _ =
       if mm = 0 orelse ! worker_trend > 50 orelse ! worker_trend < ~50 then
         max_workers := mm
-      else if ! worker_trend > 5 andalso ! max_workers < 2 * m then
+      else if ! worker_trend > 5 andalso ! max_workers < 2 * m orelse ! max_workers = 0 then
         max_workers := Int.min (mm, 2 * m)
       else ();
 
@@ -358,11 +358,11 @@
     else reraise exn;
 
 fun scheduler_loop () =
-  while
+ (while
     Multithreading.with_attributes
       (Multithreading.sync_interrupts Multithreading.public_interrupts)
       (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
-  do ();
+  do (); last_round := Time.zeroTime);
 
 fun scheduler_active () = (*requires SYNCHRONIZED*)
   (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);