# HG changeset patch # User wenzelm # Date 1313188494 -7200 # Node ID aaaa13e297dc33d017a195b9349624fb3861e228 # Parent 21f97048b478eadc4dec59bef97785648c0aa03c immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029); more careful treatment of last_round on startup/shutdown; diff -r 21f97048b478 -r aaaa13e297dc 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);