immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
more careful treatment of last_round on startup/shutdown;
--- 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);