slightly more ambitious parallelism (again);
authorwenzelm
Fri May 11 19:27:00 2018 +0200 (12 months ago)
changeset 68147a8f40dd73c61
parent 68146 d23af2dbb4e7
child 68148 fb661e4c4717
slightly more ambitious parallelism (again);
src/Pure/Concurrent/future.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Fri May 11 19:03:33 2018 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri May 11 19:27:00 2018 +0200
     1.3 @@ -584,9 +584,11 @@
     1.4  (* scheduling parameters *)
     1.5  
     1.6  fun enabled () =
     1.7 -  Multithreading.max_threads () > 1 andalso
     1.8 -    let val lim = Options.default_int "parallel_limit"
     1.9 -    in lim <= 0 orelse SYNCHRONIZED "enabled" (fn () => Task_Queue.total_jobs (! queue) < lim) end;
    1.10 +  let val threads = Multithreading.max_threads () in
    1.11 +    threads > 1 andalso
    1.12 +      let val lim = threads * Options.default_int "parallel_limit"
    1.13 +      in lim <= 0 orelse SYNCHRONIZED "enabled" (fn () => Task_Queue.total_jobs (! queue) < lim) end
    1.14 +  end;
    1.15  
    1.16  val relevant = (fn [] => false | [_] => false | _ => enabled ());
    1.17