author | wenzelm |
Sat, 06 Jun 2009 19:58:10 +0200 | |
changeset 31471 | e3987b32e401 |
parent 31311 | b82e55f51dcc |
child 31630 | 2f8ed0dca3bd |
permissions | -rw-r--r-- |
23961 | 1 |
(* Title: Pure/ML-Systems/multithreading_polyml.ML |
2 |
Author: Makarius |
|
3 |
||
31311 | 4 |
Multithreading in Poly/ML 5.2.1 or later (cf. polyml/basis/Thread.sml). |
23961 | 5 |
*) |
6 |
||
25704 | 7 |
signature MULTITHREADING_POLYML = |
8 |
sig |
|
26083
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
9 |
val interruptible: ('a -> 'b) -> 'a -> 'b |
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
10 |
val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b |
26098
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
11 |
val system_out: string -> string * int |
25704 | 12 |
structure TimeLimit: TIME_LIMIT |
13 |
end; |
|
14 |
||
15 |
signature BASIC_MULTITHREADING = |
|
16 |
sig |
|
17 |
include BASIC_MULTITHREADING |
|
18 |
include MULTITHREADING_POLYML |
|
19 |
end; |
|
20 |
||
24208 | 21 |
signature MULTITHREADING = |
22 |
sig |
|
23 |
include MULTITHREADING |
|
25704 | 24 |
include MULTITHREADING_POLYML |
24208 | 25 |
end; |
26 |
||
23961 | 27 |
structure Multithreading: MULTITHREADING = |
28 |
struct |
|
29 |
||
24072
8b9e5d776ef3
dequeue: wait loop while PROTECTED -- avoids race condition;
wenzelm
parents:
24069
diff
changeset
|
30 |
(* options *) |
24069 | 31 |
|
24119 | 32 |
val trace = ref 0; |
28465 | 33 |
|
24119 | 34 |
fun tracing level msg = |
28465 | 35 |
if level > ! trace then () |
36 |
else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr) |
|
37 |
handle _ (*sic*) => (); |
|
23961 | 38 |
|
23981 | 39 |
val available = true; |
25775
90525e67ede7
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents:
25735
diff
changeset
|
40 |
|
23973 | 41 |
val max_threads = ref 1; |
42 |
||
25775
90525e67ede7
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents:
25735
diff
changeset
|
43 |
fun max_threads_value () = |
90525e67ede7
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents:
25735
diff
changeset
|
44 |
let val m = ! max_threads |
28161 | 45 |
in if m <= 0 then Int.max (Thread.numProcessors (), 1) else m end; |
25775
90525e67ede7
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents:
25735
diff
changeset
|
46 |
|
28555 | 47 |
fun enabled () = max_threads_value () > 1; |
48 |
||
23973 | 49 |
|
24069 | 50 |
(* misc utils *) |
51 |
||
24208 | 52 |
fun show "" = "" | show name = " " ^ name; |
53 |
fun show' "" = "" | show' name = " [" ^ name ^ "]"; |
|
54 |
||
26098
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
55 |
fun read_file name = |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
56 |
let val is = TextIO.openIn name |
26504 | 57 |
in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end; |
26098
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
58 |
|
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
59 |
fun write_file name txt = |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
60 |
let val os = TextIO.openOut name |
26504 | 61 |
in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end; |
26098
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
62 |
|
24208 | 63 |
|
64 |
(* thread attributes *) |
|
65 |
||
28161 | 66 |
val no_interrupts = |
67 |
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer]; |
|
68 |
||
69 |
val regular_interrupts = |
|
70 |
[Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]; |
|
71 |
||
30612
cb6421b6a18f
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents:
30602
diff
changeset
|
72 |
val restricted_interrupts = |
cb6421b6a18f
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents:
30602
diff
changeset
|
73 |
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce]; |
cb6421b6a18f
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents:
30602
diff
changeset
|
74 |
|
28466
6e35fbfc32b8
with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
wenzelm
parents:
28465
diff
changeset
|
75 |
val safe_interrupts = map |
6e35fbfc32b8
with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
wenzelm
parents:
28465
diff
changeset
|
76 |
(fn Thread.InterruptState Thread.InterruptAsynch => |
6e35fbfc32b8
with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
wenzelm
parents:
28465
diff
changeset
|
77 |
Thread.InterruptState Thread.InterruptAsynchOnce |
6e35fbfc32b8
with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
wenzelm
parents:
28465
diff
changeset
|
78 |
| x => x); |
6e35fbfc32b8
with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
wenzelm
parents:
28465
diff
changeset
|
79 |
|
24208 | 80 |
fun with_attributes new_atts f x = |
81 |
let |
|
29550
67ec51c032cb
with_attributes: make double sure that unsafe attributes are avoided;
wenzelm
parents:
28555
diff
changeset
|
82 |
val orig_atts = safe_interrupts (Thread.getAttributes ()); |
30602
1bd90b76477a
with_attributes: canonical capture/release scheme (potentially iron out race condition);
wenzelm
parents:
29564
diff
changeset
|
83 |
val result = Exn.capture (fn () => |
1bd90b76477a
with_attributes: canonical capture/release scheme (potentially iron out race condition);
wenzelm
parents:
29564
diff
changeset
|
84 |
(Thread.setAttributes (safe_interrupts new_atts); f orig_atts x)) (); |
1bd90b76477a
with_attributes: canonical capture/release scheme (potentially iron out race condition);
wenzelm
parents:
29564
diff
changeset
|
85 |
val _ = Thread.setAttributes orig_atts; |
28466
6e35fbfc32b8
with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
wenzelm
parents:
28465
diff
changeset
|
86 |
in Exn.release result end; |
24208 | 87 |
|
28161 | 88 |
fun interruptible f = with_attributes regular_interrupts (fn _ => f); |
28150 | 89 |
|
26083
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
90 |
fun uninterruptible f = |
28150 | 91 |
with_attributes no_interrupts (fn atts => f (fn g => with_attributes atts (fn _ => g))); |
24668 | 92 |
|
24688
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
93 |
|
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
94 |
(* execution with time limit *) |
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
95 |
|
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
96 |
structure TimeLimit = |
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
97 |
struct |
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
98 |
|
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
99 |
exception TimeOut; |
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
100 |
|
26083
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
101 |
fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () => |
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
102 |
let |
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
103 |
val worker = Thread.self (); |
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
104 |
val timeout = ref false; |
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
105 |
val watchdog = Thread.fork (fn () => |
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
106 |
(OS.Process.sleep time; timeout := true; Thread.interrupt worker), []); |
24688
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
107 |
|
26083
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
108 |
val result = Exn.capture (restore_attributes f) x; |
28443 | 109 |
val was_timeout = (case result of Exn.Exn Exn.Interrupt => ! timeout | _ => false); |
24688
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
110 |
|
26083
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
111 |
val _ = Thread.interrupt watchdog handle Thread _ => (); |
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
112 |
in if was_timeout then raise TimeOut else Exn.release result end) (); |
24688
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
113 |
|
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
114 |
end; |
24668 | 115 |
|
24069 | 116 |
|
26098
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
117 |
(* system shell processes, with propagation of interrupts *) |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
118 |
|
28254
d67ba23e0277
multithreading for Poly/ML 5.1 is no longer supported;
wenzelm
parents:
28169
diff
changeset
|
119 |
fun system_out script = uninterruptible (fn restore_attributes => fn () => |
26098
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
120 |
let |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
121 |
val script_name = OS.FileSys.tmpName (); |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
122 |
val _ = write_file script_name script; |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
123 |
|
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
124 |
val pid_name = OS.FileSys.tmpName (); |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
125 |
val output_name = OS.FileSys.tmpName (); |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
126 |
|
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
127 |
(*result state*) |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
128 |
datatype result = Wait | Signal | Result of int; |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
129 |
val result = ref Wait; |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
130 |
val result_mutex = Mutex.mutex (); |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
131 |
val result_cond = ConditionVar.conditionVar (); |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
132 |
fun set_result res = |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
133 |
(Mutex.lock result_mutex; result := res; Mutex.unlock result_mutex; |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
134 |
ConditionVar.signal result_cond); |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
135 |
|
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
136 |
val _ = Mutex.lock result_mutex; |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
137 |
|
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
138 |
(*system thread*) |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
139 |
val system_thread = Thread.fork (fn () => |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
140 |
let |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
141 |
val status = |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
142 |
OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" group " ^ |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
143 |
script_name ^ " " ^ pid_name ^ " " ^ output_name); |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
144 |
val res = |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
145 |
(case Posix.Process.fromStatus status of |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
146 |
Posix.Process.W_EXITED => Result 0 |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
147 |
| Posix.Process.W_EXITSTATUS 0wx82 => Signal |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
148 |
| Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
149 |
| Posix.Process.W_SIGNALED s => |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
150 |
if s = Posix.Signal.int then Signal |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
151 |
else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
152 |
| Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); |
28398 | 153 |
in set_result res end handle _ (*sic*) => set_result (Result 2), []); |
26098
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
154 |
|
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
155 |
(*main thread -- proxy for interrupts*) |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
156 |
fun kill n = |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
157 |
(case Int.fromString (read_file pid_name) of |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
158 |
SOME pid => |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
159 |
Posix.Process.kill |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
160 |
(Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
161 |
Posix.Signal.int) |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
162 |
| NONE => ()) |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
163 |
handle OS.SysErr _ => () | IO.Io _ => |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
164 |
(OS.Process.sleep (Time.fromMilliseconds 100); if n > 0 then kill (n - 1) else ()); |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
165 |
|
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
166 |
val _ = while ! result = Wait do |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
167 |
restore_attributes (fn () => |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
168 |
(ConditionVar.waitUntil (result_cond, result_mutex, Time.now () + Time.fromMilliseconds 100); ()) |
28443 | 169 |
handle Exn.Interrupt => kill 10) (); |
26098
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
170 |
|
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
171 |
(*cleanup*) |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
172 |
val output = read_file output_name handle IO.Io _ => ""; |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
173 |
val _ = OS.FileSys.remove script_name handle OS.SysErr _ => (); |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
174 |
val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => (); |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
175 |
val _ = OS.FileSys.remove output_name handle OS.SysErr _ => (); |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
176 |
val _ = Thread.interrupt system_thread handle Thread _ => (); |
28443 | 177 |
val rc = (case ! result of Signal => raise Exn.Interrupt | Result rc => rc); |
26098
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
178 |
in (output, rc) end) (); |
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
179 |
|
b59d33f73aed
added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents:
26083
diff
changeset
|
180 |
|
23961 | 181 |
(* critical section -- may be nested within the same thread *) |
182 |
||
183 |
local |
|
184 |
||
24063 | 185 |
val critical_lock = Mutex.mutex (); |
186 |
val critical_thread = ref (NONE: Thread.thread option); |
|
187 |
val critical_name = ref ""; |
|
188 |
||
23961 | 189 |
in |
190 |
||
191 |
fun self_critical () = |
|
192 |
(case ! critical_thread of |
|
193 |
NONE => false |
|
28150 | 194 |
| SOME t => Thread.equal (t, Thread.self ())); |
23961 | 195 |
|
23991 | 196 |
fun NAMED_CRITICAL name e = |
23961 | 197 |
if self_critical () then e () |
198 |
else |
|
26083
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
199 |
uninterruptible (fn restore_attributes => fn () => |
24208 | 200 |
let |
201 |
val name' = ! critical_name; |
|
202 |
val _ = |
|
203 |
if Mutex.trylock critical_lock then () |
|
204 |
else |
|
205 |
let |
|
206 |
val timer = Timer.startRealTimer (); |
|
207 |
val _ = tracing 4 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting"); |
|
208 |
val _ = Mutex.lock critical_lock; |
|
209 |
val time = Timer.checkRealTimer timer; |
|
26493
de4764e95166
CRITICAL: further trace levels for 1000ms and 100ms;
wenzelm
parents:
26390
diff
changeset
|
210 |
val trace_time = |
de4764e95166
CRITICAL: further trace levels for 1000ms and 100ms;
wenzelm
parents:
26390
diff
changeset
|
211 |
if Time.>= (time, Time.fromMilliseconds 1000) then 1 |
de4764e95166
CRITICAL: further trace levels for 1000ms and 100ms;
wenzelm
parents:
26390
diff
changeset
|
212 |
else if Time.>= (time, Time.fromMilliseconds 100) then 2 |
de4764e95166
CRITICAL: further trace levels for 1000ms and 100ms;
wenzelm
parents:
26390
diff
changeset
|
213 |
else if Time.>= (time, Time.fromMilliseconds 10) then 3 else 4; |
de4764e95166
CRITICAL: further trace levels for 1000ms and 100ms;
wenzelm
parents:
26390
diff
changeset
|
214 |
val _ = tracing trace_time (fn () => |
24208 | 215 |
"CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time); |
216 |
in () end; |
|
217 |
val _ = critical_thread := SOME (Thread.self ()); |
|
218 |
val _ = critical_name := name; |
|
26083
abb3f8dd66dc
removed managed_process (cf. General/shell_process.ML);
wenzelm
parents:
26074
diff
changeset
|
219 |
val result = Exn.capture (restore_attributes e) (); |
24208 | 220 |
val _ = critical_name := ""; |
221 |
val _ = critical_thread := NONE; |
|
222 |
val _ = Mutex.unlock critical_lock; |
|
223 |
in Exn.release result end) (); |
|
23961 | 224 |
|
23991 | 225 |
fun CRITICAL e = NAMED_CRITICAL "" e; |
23981 | 226 |
|
23961 | 227 |
end; |
228 |
||
23973 | 229 |
|
25704 | 230 |
(* serial numbers *) |
231 |
||
232 |
local |
|
233 |
||
234 |
val serial_lock = Mutex.mutex (); |
|
235 |
val serial_count = ref 0; |
|
236 |
||
237 |
in |
|
238 |
||
239 |
val serial = uninterruptible (fn _ => fn () => |
|
240 |
let |
|
241 |
val _ = Mutex.lock serial_lock; |
|
28124
10a1f1f4c6ae
moved Multithreading.task/schedule to Concurrent/schedule.ML;
wenzelm
parents:
26504
diff
changeset
|
242 |
val _ = serial_count := ! serial_count + 1; |
10a1f1f4c6ae
moved Multithreading.task/schedule to Concurrent/schedule.ML;
wenzelm
parents:
26504
diff
changeset
|
243 |
val res = ! serial_count; |
25704 | 244 |
val _ = Mutex.unlock serial_lock; |
245 |
in res end); |
|
246 |
||
23961 | 247 |
end; |
248 |
||
25704 | 249 |
end; |
24688
a5754ca5c510
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
24672
diff
changeset
|
250 |
|
25704 | 251 |
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading; |
252 |
open BasicMultithreading; |