--- a/src/Pure/ML-Systems/multithreading_polyml.ML Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Wed Dec 11 18:02:22 2013 +0100
@@ -25,21 +25,6 @@
structure Multithreading: MULTITHREADING =
struct
-(* options *)
-
-val available = true;
-
-val max_threads = ref 1;
-
-fun max_threads_value () =
- let val m = ! max_threads in
- if m > 0 then m
- else Int.min (Int.max (Thread.numProcessors (), 1), 8)
- end;
-
-fun enabled () = max_threads_value () > 1;
-
-
(* thread attributes *)
val no_interrupts =
@@ -90,6 +75,37 @@
f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
+(* options *)
+
+val available = true;
+
+fun max_threads_result m =
+ if m > 0 then m
+ else
+ let val n =
+ (case Thread.numPhysicalProcessors () of
+ SOME n => n
+ | NONE => Thread.numProcessors ())
+ in Int.min (Int.max (n, 1), 8) end;
+
+val max_threads = ref 1;
+
+fun max_threads_value () = ! max_threads;
+
+fun max_threads_update m = max_threads := max_threads_result m;
+
+fun max_threads_setmp m f x =
+ uninterruptible (fn restore_attributes => fn () =>
+ let
+ val max_threads_orig = ! max_threads;
+ val _ = max_threads_update m;
+ val result = Exn.capture (restore_attributes f) x;
+ val _ = max_threads := max_threads_orig;
+ in Exn.release result end) ();
+
+fun enabled () = max_threads_value () > 1;
+
+
(* synchronous wait *)
fun sync_wait opt_atts time cond lock =