1.1 --- a/src/Pure/Concurrent/future.ML	Wed Nov 04 21:21:05 2009 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Nov 04 21:22:35 2009 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4            else if Task_Queue.cancel (! queue) group then ()
     1.5            else do_cancel group;
     1.6          val _ = broadcast work_finished;
     1.7 -        val _ = if maximal then () else broadcast work_available;
     1.8 +        val _ = if maximal then () else signal work_available;
     1.9        in () end);
    1.10    in () end;
    1.11  
    1.12 @@ -216,7 +216,7 @@
    1.13    else
    1.14      (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of
    1.15        NONE => (worker_wait false work_available; worker_next true)
    1.16 -    | some => some);
    1.17 +    | some => (signal work_available; some));
    1.18  
    1.19  fun worker_loop name =
    1.20    (case SYNCHRONIZED name (fn () => worker_next false) of
    1.21 @@ -281,7 +281,7 @@
    1.22      val mm =
    1.23        if ! do_shutdown then 0
    1.24        else if m = 9999 then 1
    1.25 -      else Int.min (Int.max (count_workers Working + 2 * count_workers Waiting, m), 2 * m);
    1.26 +      else Int.min (Int.max (count_workers Working + 2 * count_workers Waiting, m), 4 * m);
    1.27      val _ =
    1.28        if tick andalso mm > ! max_workers then
    1.29          Unsynchronized.change worker_trend (fn w => if w < 0 then 0 else w + 1)
    1.30 @@ -289,8 +289,8 @@
    1.31          Unsynchronized.change worker_trend (fn w => if w > 0 then 0 else w - 1)
    1.32        else ();
    1.33      val _ =
    1.34 -      if mm = 0 orelse ! worker_trend > 5 orelse ! worker_trend < ~50
    1.35 -      then max_workers := mm
    1.36 +      if mm = 0 orelse ! worker_trend > 50 orelse ! worker_trend < ~50 then max_workers := mm
    1.37 +      else if ! worker_trend > 5 then max_workers := Int.min (mm, 2 * m)
    1.38        else ();
    1.39  
    1.40      val missing = ! max_workers - length (! workers);