added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
authorwenzelm
Wed Jan 02 16:32:53 2008 +0100 (2008-01-02 ago)
changeset 2577590525e67ede7
parent 25774 28fac5c2af54
child 25776 4e4eb0f87850
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
src/Pure/ML-Systems/multithreading.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/ML-Systems/multithreading.ML	Wed Jan 02 16:32:52 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Wed Jan 02 16:32:53 2008 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4    val tracing: int -> (unit -> string) -> unit
     1.5    val available: bool
     1.6    val max_threads: int ref
     1.7 +  val max_threads_value: unit -> int
     1.8    val self_critical: unit -> bool
     1.9    datatype 'a task =
    1.10      Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    1.11 @@ -37,6 +38,7 @@
    1.12  
    1.13  val available = false;
    1.14  val max_threads = ref (1: int);
    1.15 +fun max_threads_value () = Int.max (! max_threads, 1);
    1.16  
    1.17  
    1.18  (* critical section *)
     2.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jan 02 16:32:52 2008 +0100
     2.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jan 02 16:32:53 2008 +0100
     2.3 @@ -38,8 +38,13 @@
     2.4    else ();
     2.5  
     2.6  val available = true;
     2.7 +
     2.8  val max_threads = ref 1;
     2.9  
    2.10 +fun max_threads_value () =
    2.11 +  let val m = ! max_threads
    2.12 +  in if m <= 0 then Thread.numProcessors () else m end;
    2.13 +
    2.14  
    2.15  (* misc utils *)
    2.16  
     3.1 --- a/src/Pure/Thy/thy_info.ML	Wed Jan 02 16:32:52 2008 +0100
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Jan 02 16:32:53 2008 +0100
     3.3 @@ -377,7 +377,7 @@
     3.4  in
     3.5  
     3.6  fun schedule_tasks tasks n =
     3.7 -  let val m = ! Multithreading.max_threads in
     3.8 +  let val m = Multithreading.max_threads_value () in
     3.9      if m <= 1 orelse n <= 1 then schedule_seq tasks
    3.10      else if Multithreading.self_critical () then
    3.11       (warning (loader_msg "no multithreading within critical section" []);