author | wenzelm |
Thu, 03 Mar 2016 21:59:21 +0100 | |
changeset 62508 | d0b68218ea55 |
parent 62501 | src/Pure/RAW/multithreading.ML@98fa1f9a292f |
child 62715 | 8312e5d8d217 |
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 |
|
62359 | 7 |
signature BASIC_MULTITHREADING = |
8 |
sig |
|
9 |
val interruptible: ('a -> 'b) -> 'a -> 'b |
|
10 |
val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b |
|
11 |
end; |
|
12 |
||
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
13 |
signature MULTITHREADING = |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
14 |
sig |
62359 | 15 |
include BASIC_MULTITHREADING |
28149 | 16 |
val no_interrupts: Thread.threadAttribute list |
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
17 |
val public_interrupts: Thread.threadAttribute list |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
18 |
val private_interrupts: Thread.threadAttribute list |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
19 |
val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list |
41713
a21084741b37
added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
wenzelm
parents:
39616
diff
changeset
|
20 |
val interrupted: unit -> unit (*exception Interrupt*) |
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
21 |
val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a |
62359 | 22 |
val max_threads_value: unit -> int |
23 |
val max_threads_update: int -> unit |
|
24 |
val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b |
|
25 |
val enabled: unit -> bool |
|
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
26 |
val sync_wait: Thread.threadAttribute list option -> Time.time option -> |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
27 |
ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result |
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
32777
diff
changeset
|
28 |
val trace: int ref |
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
29 |
val tracing: int -> (unit -> string) -> unit |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
30 |
val tracing_time: bool -> Time.time -> (unit -> string) -> unit |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
31 |
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
|
32 |
val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a |
25704 | 33 |
val serial: unit -> int |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
34 |
end; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
35 |
|
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
36 |
structure Multithreading: MULTITHREADING = |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
37 |
struct |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
38 |
|
62359 | 39 |
(* thread attributes *) |
40 |
||
41 |
val no_interrupts = |
|
42 |
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer]; |
|
43 |
||
44 |
val test_interrupts = |
|
45 |
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch]; |
|
46 |
||
47 |
val public_interrupts = |
|
48 |
[Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]; |
|
49 |
||
50 |
val private_interrupts = |
|
51 |
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce]; |
|
52 |
||
53 |
val sync_interrupts = map |
|
54 |
(fn x as Thread.InterruptState Thread.InterruptDefer => x |
|
55 |
| Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch |
|
56 |
| x => x); |
|
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
57 |
|
62359 | 58 |
val safe_interrupts = map |
59 |
(fn Thread.InterruptState Thread.InterruptAsynch => |
|
60 |
Thread.InterruptState Thread.InterruptAsynchOnce |
|
61 |
| x => x); |
|
62 |
||
63 |
fun interrupted () = |
|
64 |
let |
|
65 |
val orig_atts = safe_interrupts (Thread.getAttributes ()); |
|
66 |
val _ = Thread.setAttributes test_interrupts; |
|
67 |
val test = Exn.capture Thread.testInterrupt (); |
|
68 |
val _ = Thread.setAttributes orig_atts; |
|
69 |
in Exn.release test end; |
|
70 |
||
71 |
fun with_attributes new_atts e = |
|
72 |
let |
|
73 |
val orig_atts = safe_interrupts (Thread.getAttributes ()); |
|
74 |
val result = Exn.capture (fn () => |
|
75 |
(Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) (); |
|
76 |
val _ = Thread.setAttributes orig_atts; |
|
77 |
in Exn.release result end; |
|
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
78 |
|
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
|
79 |
|
62359 | 80 |
(* portable wrappers *) |
81 |
||
82 |
fun interruptible f x = with_attributes public_interrupts (fn _ => f x); |
|
83 |
||
84 |
fun uninterruptible f x = |
|
85 |
with_attributes no_interrupts (fn atts => |
|
86 |
f (fn g => fn y => with_attributes atts (fn _ => g y)) x); |
|
87 |
||
88 |
||
89 |
(* options *) |
|
90 |
||
62501 | 91 |
fun num_processors () = |
92 |
(case Thread.numPhysicalProcessors () of |
|
93 |
SOME n => n |
|
94 |
| NONE => Thread.numProcessors ()); |
|
95 |
||
62359 | 96 |
fun max_threads_result m = |
62501 | 97 |
if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8); |
62359 | 98 |
|
99 |
val max_threads = ref 1; |
|
100 |
||
101 |
fun max_threads_value () = ! max_threads; |
|
102 |
||
103 |
fun max_threads_update m = max_threads := max_threads_result m; |
|
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
|
104 |
|
62359 | 105 |
fun max_threads_setmp m f x = |
106 |
uninterruptible (fn restore_attributes => fn () => |
|
107 |
let |
|
108 |
val max_threads_orig = ! max_threads; |
|
109 |
val _ = max_threads_update m; |
|
110 |
val result = Exn.capture (restore_attributes f) x; |
|
111 |
val _ = max_threads := max_threads_orig; |
|
112 |
in Exn.release result end) (); |
|
113 |
||
114 |
fun enabled () = max_threads_value () > 1; |
|
28187
4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset
|
115 |
|
62359 | 116 |
|
117 |
(* synchronous wait *) |
|
41713
a21084741b37
added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
wenzelm
parents:
39616
diff
changeset
|
118 |
|
62359 | 119 |
fun sync_wait opt_atts time cond lock = |
120 |
with_attributes |
|
121 |
(sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ())) |
|
122 |
(fn _ => |
|
123 |
(case time of |
|
124 |
SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t)) |
|
125 |
| NONE => (ConditionVar.wait (cond, lock); Exn.Res true)) |
|
126 |
handle exn => Exn.Exn exn); |
|
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
127 |
|
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
128 |
|
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
129 |
(* tracing *) |
30612
cb6421b6a18f
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents:
29564
diff
changeset
|
130 |
|
62359 | 131 |
val trace = ref 0; |
132 |
||
133 |
fun tracing level msg = |
|
134 |
if level > ! trace then () |
|
135 |
else uninterruptible (fn _ => fn () => |
|
136 |
(TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr) |
|
137 |
handle _ (*sic*) => ()) (); |
|
138 |
||
139 |
fun tracing_time detailed time = |
|
140 |
tracing |
|
141 |
(if not detailed then 5 |
|
142 |
else if Time.>= (time, seconds 1.0) then 1 |
|
143 |
else if Time.>= (time, seconds 0.1) then 2 |
|
144 |
else if Time.>= (time, seconds 0.01) then 3 |
|
145 |
else if Time.>= (time, seconds 0.001) then 4 else 5); |
|
146 |
||
147 |
fun real_time f x = |
|
148 |
let |
|
149 |
val timer = Timer.startRealTimer (); |
|
150 |
val () = f x; |
|
151 |
val time = Timer.checkRealTimer timer; |
|
152 |
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
|
153 |
|
25735 | 154 |
|
59180
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59054
diff
changeset
|
155 |
(* synchronized evaluation *) |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
156 |
|
62359 | 157 |
fun synchronized name lock e = |
158 |
Exn.release (uninterruptible (fn restore_attributes => fn () => |
|
159 |
let |
|
160 |
val immediate = |
|
161 |
if Mutex.trylock lock then true |
|
162 |
else |
|
163 |
let |
|
164 |
val _ = tracing 5 (fn () => name ^ ": locking ..."); |
|
165 |
val time = real_time Mutex.lock lock; |
|
166 |
val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time); |
|
167 |
in false end; |
|
168 |
val result = Exn.capture (restore_attributes e) (); |
|
169 |
val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ..."); |
|
170 |
val _ = Mutex.unlock lock; |
|
171 |
in result end) ()); |
|
59054
61b723761dff
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents:
54717
diff
changeset
|
172 |
|
25735 | 173 |
|
174 |
(* serial numbers *) |
|
175 |
||
62359 | 176 |
local |
177 |
||
178 |
val serial_lock = Mutex.mutex (); |
|
179 |
val serial_count = ref 0; |
|
180 |
||
181 |
in |
|
182 |
||
183 |
val serial = uninterruptible (fn _ => fn () => |
|
184 |
let |
|
185 |
val _ = Mutex.lock serial_lock; |
|
186 |
val _ = serial_count := ! serial_count + 1; |
|
187 |
val res = ! serial_count; |
|
188 |
val _ = Mutex.unlock serial_lock; |
|
189 |
in res end); |
|
25704 | 190 |
|
28123
53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset
|
191 |
end; |
53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset
|
192 |
|
62359 | 193 |
end; |
194 |
||
195 |
structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading; |
|
196 |
open Basic_Multithreading; |