author | wenzelm |
Sat, 09 Apr 2016 14:21:29 +0200 | |
changeset 62926 | 9ff9bcbc2341 |
parent 62925 | f1bdf10f95d8 |
child 62927 | bb2b8e915243 |
permissions | -rw-r--r-- |
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
1 |
(* Title: Pure/Concurrent/multithreading.ML |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
3 |
|
62359 | 4 |
Multithreading in Poly/ML (cf. polyml/basis/Thread.sml). |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
5 |
*) |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
6 |
|
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
7 |
signature MULTITHREADING = |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
8 |
sig |
62925 | 9 |
val max_threads: unit -> int |
62359 | 10 |
val max_threads_update: int -> unit |
11 |
val enabled: unit -> bool |
|
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
12 |
val sync_wait: Thread.threadAttribute list option -> Time.time option -> |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
13 |
ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result |
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
32777
diff
changeset
|
14 |
val trace: int ref |
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
15 |
val tracing: int -> (unit -> string) -> unit |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
16 |
val tracing_time: bool -> Time.time -> (unit -> string) -> unit |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
17 |
val real_time: ('a -> unit) -> 'a -> Time.time |
59054
61b723761dff
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents:
54717
diff
changeset
|
18 |
val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
19 |
end; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
20 |
|
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
21 |
structure Multithreading: MULTITHREADING = |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
22 |
struct |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
23 |
|
62925 | 24 |
(* max_threads *) |
25 |
||
26 |
local |
|
62359 | 27 |
|
62501 | 28 |
fun num_processors () = |
29 |
(case Thread.numPhysicalProcessors () of |
|
30 |
SOME n => n |
|
31 |
| NONE => Thread.numProcessors ()); |
|
32 |
||
62359 | 33 |
fun max_threads_result m = |
62926
9ff9bcbc2341
virtual Pure is single-threaded to avoid confusion with multiple thread farms etc.;
wenzelm
parents:
62925
diff
changeset
|
34 |
if Thread_Data.is_virtual then 1 |
9ff9bcbc2341
virtual Pure is single-threaded to avoid confusion with multiple thread farms etc.;
wenzelm
parents:
62925
diff
changeset
|
35 |
else if m > 0 then m |
9ff9bcbc2341
virtual Pure is single-threaded to avoid confusion with multiple thread farms etc.;
wenzelm
parents:
62925
diff
changeset
|
36 |
else Int.min (Int.max (num_processors (), 1), 8); |
62359 | 37 |
|
62925 | 38 |
val max_threads_state = ref 1; |
39 |
||
40 |
in |
|
32286
1fb5db48002d
added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
wenzelm
parents:
32186
diff
changeset
|
41 |
|
62925 | 42 |
fun max_threads () = ! max_threads_state; |
43 |
fun max_threads_update m = max_threads_state := max_threads_result m; |
|
44 |
fun enabled () = max_threads () > 1; |
|
45 |
||
46 |
end; |
|
28187
4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset
|
47 |
|
62359 | 48 |
|
49 |
(* synchronous wait *) |
|
41713
a21084741b37
added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
wenzelm
parents:
39616
diff
changeset
|
50 |
|
62359 | 51 |
fun sync_wait opt_atts time cond lock = |
62923 | 52 |
Thread_Attributes.with_attributes |
53 |
(Thread_Attributes.sync_interrupts |
|
54 |
(case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ())) |
|
62359 | 55 |
(fn _ => |
56 |
(case time of |
|
57 |
SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t)) |
|
58 |
| NONE => (ConditionVar.wait (cond, lock); Exn.Res true)) |
|
59 |
handle exn => Exn.Exn exn); |
|
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
60 |
|
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
61 |
|
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
62 |
(* tracing *) |
30612
cb6421b6a18f
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents:
29564
diff
changeset
|
63 |
|
62359 | 64 |
val trace = ref 0; |
65 |
||
66 |
fun tracing level msg = |
|
67 |
if level > ! trace then () |
|
62923 | 68 |
else Thread_Attributes.uninterruptible (fn _ => fn () => |
62359 | 69 |
(TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr) |
70 |
handle _ (*sic*) => ()) (); |
|
71 |
||
72 |
fun tracing_time detailed time = |
|
73 |
tracing |
|
74 |
(if not detailed then 5 |
|
62826 | 75 |
else if time >= seconds 1.0 then 1 |
76 |
else if time >= seconds 0.1 then 2 |
|
77 |
else if time >= seconds 0.01 then 3 |
|
78 |
else if time >= seconds 0.001 then 4 else 5); |
|
62359 | 79 |
|
80 |
fun real_time f x = |
|
81 |
let |
|
82 |
val timer = Timer.startRealTimer (); |
|
83 |
val () = f x; |
|
84 |
val time = Timer.checkRealTimer timer; |
|
85 |
in time end; |
|
32286
1fb5db48002d
added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
wenzelm
parents:
32186
diff
changeset
|
86 |
|
25735 | 87 |
|
59180
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59054
diff
changeset
|
88 |
(* synchronized evaluation *) |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
89 |
|
62359 | 90 |
fun synchronized name lock e = |
62923 | 91 |
Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () => |
62359 | 92 |
let |
93 |
val immediate = |
|
94 |
if Mutex.trylock lock then true |
|
95 |
else |
|
96 |
let |
|
97 |
val _ = tracing 5 (fn () => name ^ ": locking ..."); |
|
98 |
val time = real_time Mutex.lock lock; |
|
99 |
val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time); |
|
100 |
in false end; |
|
101 |
val result = Exn.capture (restore_attributes e) (); |
|
102 |
val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ..."); |
|
103 |
val _ = Mutex.unlock lock; |
|
104 |
in result end) ()); |
|
59054
61b723761dff
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents:
54717
diff
changeset
|
105 |
|
28123
53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset
|
106 |
end; |