wenzelm@23961
|
1 |
(* Title: Pure/ML-Systems/multithreading_polyml.ML
|
wenzelm@23961
|
2 |
ID: $Id$
|
wenzelm@23961
|
3 |
Author: Makarius
|
wenzelm@23961
|
4 |
|
wenzelm@25704
|
5 |
Multithreading in Poly/ML 5.1 (cf. polyml/basis/Thread.sml).
|
wenzelm@23961
|
6 |
*)
|
wenzelm@23961
|
7 |
|
wenzelm@23961
|
8 |
open Thread;
|
wenzelm@23961
|
9 |
|
wenzelm@25704
|
10 |
signature MULTITHREADING_POLYML =
|
wenzelm@25704
|
11 |
sig
|
wenzelm@26083
|
12 |
val interruptible: ('a -> 'b) -> 'a -> 'b
|
wenzelm@26083
|
13 |
val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
|
wenzelm@26098
|
14 |
val system_out: string -> string * int
|
wenzelm@25704
|
15 |
structure TimeLimit: TIME_LIMIT
|
wenzelm@25704
|
16 |
end;
|
wenzelm@25704
|
17 |
|
wenzelm@25704
|
18 |
signature BASIC_MULTITHREADING =
|
wenzelm@25704
|
19 |
sig
|
wenzelm@25704
|
20 |
include BASIC_MULTITHREADING
|
wenzelm@25704
|
21 |
include MULTITHREADING_POLYML
|
wenzelm@25704
|
22 |
end;
|
wenzelm@25704
|
23 |
|
wenzelm@24208
|
24 |
signature MULTITHREADING =
|
wenzelm@24208
|
25 |
sig
|
wenzelm@24208
|
26 |
include MULTITHREADING
|
wenzelm@25704
|
27 |
include MULTITHREADING_POLYML
|
wenzelm@24208
|
28 |
end;
|
wenzelm@24208
|
29 |
|
wenzelm@23961
|
30 |
structure Multithreading: MULTITHREADING =
|
wenzelm@23961
|
31 |
struct
|
wenzelm@23961
|
32 |
|
wenzelm@24072
|
33 |
(* options *)
|
wenzelm@24069
|
34 |
|
wenzelm@24119
|
35 |
val trace = ref 0;
|
wenzelm@24119
|
36 |
fun tracing level msg =
|
wenzelm@24119
|
37 |
if level <= ! trace
|
wenzelm@23981
|
38 |
then (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
|
wenzelm@23981
|
39 |
else ();
|
wenzelm@23961
|
40 |
|
wenzelm@23981
|
41 |
val available = true;
|
wenzelm@25775
|
42 |
|
wenzelm@23973
|
43 |
val max_threads = ref 1;
|
wenzelm@23973
|
44 |
|
wenzelm@25775
|
45 |
fun max_threads_value () =
|
wenzelm@25775
|
46 |
let val m = ! max_threads
|
wenzelm@25775
|
47 |
in if m <= 0 then Thread.numProcessors () else m end;
|
wenzelm@25775
|
48 |
|
wenzelm@23973
|
49 |
|
wenzelm@24069
|
50 |
(* misc utils *)
|
wenzelm@24069
|
51 |
|
wenzelm@24208
|
52 |
fun cons x xs = x :: xs;
|
wenzelm@24069
|
53 |
|
wenzelm@24208
|
54 |
fun change r f = r := f (! r);
|
wenzelm@24069
|
55 |
|
wenzelm@24069
|
56 |
fun inc i = (i := ! i + 1; ! i);
|
wenzelm@24069
|
57 |
fun dec i = (i := ! i - 1; ! i);
|
wenzelm@24069
|
58 |
|
wenzelm@24208
|
59 |
fun show "" = "" | show name = " " ^ name;
|
wenzelm@24208
|
60 |
fun show' "" = "" | show' name = " [" ^ name ^ "]";
|
wenzelm@24208
|
61 |
|
wenzelm@26098
|
62 |
fun read_file name =
|
wenzelm@26098
|
63 |
let val is = TextIO.openIn name
|
wenzelm@26098
|
64 |
in TextIO.inputAll is before TextIO.closeIn is end;
|
wenzelm@26098
|
65 |
|
wenzelm@26098
|
66 |
fun write_file name txt =
|
wenzelm@26098
|
67 |
let val os = TextIO.openOut name
|
wenzelm@26098
|
68 |
in TextIO.output (os, txt) before TextIO.closeOut os end;
|
wenzelm@26098
|
69 |
|
wenzelm@24208
|
70 |
|
wenzelm@24208
|
71 |
(* thread attributes *)
|
wenzelm@24208
|
72 |
|
wenzelm@24208
|
73 |
fun with_attributes new_atts f x =
|
wenzelm@24208
|
74 |
let
|
wenzelm@24208
|
75 |
val orig_atts = Thread.getAttributes ();
|
wenzelm@24208
|
76 |
fun restore () = Thread.setAttributes orig_atts;
|
wenzelm@24208
|
77 |
in
|
wenzelm@24208
|
78 |
Exn.release
|
wenzelm@24214
|
79 |
(*RACE for fully asynchronous interrupts!*)
|
wenzelm@24214
|
80 |
(let
|
wenzelm@24208
|
81 |
val _ = Thread.setAttributes new_atts;
|
wenzelm@24214
|
82 |
val result = Exn.capture (f orig_atts) x;
|
wenzelm@24208
|
83 |
val _ = restore ();
|
wenzelm@24208
|
84 |
in result end
|
wenzelm@24208
|
85 |
handle Interrupt => (restore (); Exn.Exn Interrupt))
|
wenzelm@24208
|
86 |
end;
|
wenzelm@24208
|
87 |
|
wenzelm@26083
|
88 |
fun interruptible f =
|
wenzelm@26083
|
89 |
with_attributes
|
wenzelm@26083
|
90 |
[Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]
|
wenzelm@26083
|
91 |
(fn _ => f);
|
wenzelm@24668
|
92 |
|
wenzelm@26083
|
93 |
fun uninterruptible f =
|
wenzelm@26083
|
94 |
with_attributes
|
wenzelm@26083
|
95 |
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer]
|
wenzelm@26083
|
96 |
(fn atts => f (fn g => with_attributes atts (fn _ => g)));
|
wenzelm@24668
|
97 |
|
wenzelm@24688
|
98 |
|
wenzelm@24688
|
99 |
(* execution with time limit *)
|
wenzelm@24688
|
100 |
|
wenzelm@24688
|
101 |
structure TimeLimit =
|
wenzelm@24688
|
102 |
struct
|
wenzelm@24688
|
103 |
|
wenzelm@24688
|
104 |
exception TimeOut;
|
wenzelm@24688
|
105 |
|
wenzelm@26083
|
106 |
fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
|
wenzelm@26083
|
107 |
let
|
wenzelm@26083
|
108 |
val worker = Thread.self ();
|
wenzelm@26083
|
109 |
val timeout = ref false;
|
wenzelm@26083
|
110 |
val watchdog = Thread.fork (fn () =>
|
wenzelm@26083
|
111 |
(OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
|
wenzelm@24688
|
112 |
|
wenzelm@26083
|
113 |
(*RACE! timeout signal vs. external Interrupt*)
|
wenzelm@26083
|
114 |
val result = Exn.capture (restore_attributes f) x;
|
wenzelm@26083
|
115 |
val was_timeout = (case result of Exn.Exn Interrupt => ! timeout | _ => false);
|
wenzelm@24688
|
116 |
|
wenzelm@26083
|
117 |
val _ = Thread.interrupt watchdog handle Thread _ => ();
|
wenzelm@26083
|
118 |
in if was_timeout then raise TimeOut else Exn.release result end) ();
|
wenzelm@24688
|
119 |
|
wenzelm@24688
|
120 |
end;
|
wenzelm@24668
|
121 |
|
wenzelm@24069
|
122 |
|
wenzelm@26098
|
123 |
(* system shell processes, with propagation of interrupts *)
|
wenzelm@26098
|
124 |
|
wenzelm@26221
|
125 |
fun system_out_threaded script = uninterruptible (fn restore_attributes => fn () =>
|
wenzelm@26098
|
126 |
let
|
wenzelm@26098
|
127 |
val script_name = OS.FileSys.tmpName ();
|
wenzelm@26098
|
128 |
val _ = write_file script_name script;
|
wenzelm@26098
|
129 |
|
wenzelm@26098
|
130 |
val pid_name = OS.FileSys.tmpName ();
|
wenzelm@26098
|
131 |
val output_name = OS.FileSys.tmpName ();
|
wenzelm@26098
|
132 |
|
wenzelm@26098
|
133 |
(*result state*)
|
wenzelm@26098
|
134 |
datatype result = Wait | Signal | Result of int;
|
wenzelm@26098
|
135 |
val result = ref Wait;
|
wenzelm@26098
|
136 |
val result_mutex = Mutex.mutex ();
|
wenzelm@26098
|
137 |
val result_cond = ConditionVar.conditionVar ();
|
wenzelm@26098
|
138 |
fun set_result res =
|
wenzelm@26098
|
139 |
(Mutex.lock result_mutex; result := res; Mutex.unlock result_mutex;
|
wenzelm@26098
|
140 |
ConditionVar.signal result_cond);
|
wenzelm@26098
|
141 |
|
wenzelm@26098
|
142 |
val _ = Mutex.lock result_mutex;
|
wenzelm@26098
|
143 |
|
wenzelm@26098
|
144 |
(*system thread*)
|
wenzelm@26098
|
145 |
val system_thread = Thread.fork (fn () =>
|
wenzelm@26098
|
146 |
let
|
wenzelm@26098
|
147 |
val status =
|
wenzelm@26098
|
148 |
OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" group " ^
|
wenzelm@26098
|
149 |
script_name ^ " " ^ pid_name ^ " " ^ output_name);
|
wenzelm@26098
|
150 |
val res =
|
wenzelm@26098
|
151 |
(case Posix.Process.fromStatus status of
|
wenzelm@26098
|
152 |
Posix.Process.W_EXITED => Result 0
|
wenzelm@26098
|
153 |
| Posix.Process.W_EXITSTATUS 0wx82 => Signal
|
wenzelm@26098
|
154 |
| Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
|
wenzelm@26098
|
155 |
| Posix.Process.W_SIGNALED s =>
|
wenzelm@26098
|
156 |
if s = Posix.Signal.int then Signal
|
wenzelm@26098
|
157 |
else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
|
wenzelm@26098
|
158 |
| Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
|
wenzelm@26098
|
159 |
in set_result res end handle _ => set_result (Result 2), []);
|
wenzelm@26098
|
160 |
|
wenzelm@26098
|
161 |
(*main thread -- proxy for interrupts*)
|
wenzelm@26098
|
162 |
fun kill n =
|
wenzelm@26098
|
163 |
(case Int.fromString (read_file pid_name) of
|
wenzelm@26098
|
164 |
SOME pid =>
|
wenzelm@26098
|
165 |
Posix.Process.kill
|
wenzelm@26098
|
166 |
(Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
|
wenzelm@26098
|
167 |
Posix.Signal.int)
|
wenzelm@26098
|
168 |
| NONE => ())
|
wenzelm@26098
|
169 |
handle OS.SysErr _ => () | IO.Io _ =>
|
wenzelm@26098
|
170 |
(OS.Process.sleep (Time.fromMilliseconds 100); if n > 0 then kill (n - 1) else ());
|
wenzelm@26098
|
171 |
|
wenzelm@26098
|
172 |
val _ = while ! result = Wait do
|
wenzelm@26098
|
173 |
restore_attributes (fn () =>
|
wenzelm@26098
|
174 |
(ConditionVar.waitUntil (result_cond, result_mutex, Time.now () + Time.fromMilliseconds 100); ())
|
wenzelm@26098
|
175 |
handle Interrupt => kill 10) ();
|
wenzelm@26098
|
176 |
|
wenzelm@26098
|
177 |
(*cleanup*)
|
wenzelm@26098
|
178 |
val output = read_file output_name handle IO.Io _ => "";
|
wenzelm@26098
|
179 |
val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
|
wenzelm@26098
|
180 |
val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
|
wenzelm@26098
|
181 |
val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
|
wenzelm@26098
|
182 |
val _ = Thread.interrupt system_thread handle Thread _ => ();
|
wenzelm@26098
|
183 |
val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
|
wenzelm@26098
|
184 |
in (output, rc) end) ();
|
wenzelm@26098
|
185 |
|
wenzelm@26221
|
186 |
val system_out =
|
wenzelm@26221
|
187 |
if ml_system = "polyml-5.1" then system_out (*signals not propagated from root thread!*)
|
wenzelm@26221
|
188 |
else system_out_threaded;
|
wenzelm@26221
|
189 |
|
wenzelm@26098
|
190 |
|
wenzelm@23961
|
191 |
(* critical section -- may be nested within the same thread *)
|
wenzelm@23961
|
192 |
|
wenzelm@23961
|
193 |
local
|
wenzelm@23961
|
194 |
|
wenzelm@24063
|
195 |
val critical_lock = Mutex.mutex ();
|
wenzelm@24063
|
196 |
val critical_thread = ref (NONE: Thread.thread option);
|
wenzelm@24063
|
197 |
val critical_name = ref "";
|
wenzelm@24063
|
198 |
|
wenzelm@23961
|
199 |
in
|
wenzelm@23961
|
200 |
|
wenzelm@23961
|
201 |
fun self_critical () =
|
wenzelm@23961
|
202 |
(case ! critical_thread of
|
wenzelm@23961
|
203 |
NONE => false
|
wenzelm@23961
|
204 |
| SOME id => Thread.equal (id, Thread.self ()));
|
wenzelm@23961
|
205 |
|
wenzelm@23991
|
206 |
fun NAMED_CRITICAL name e =
|
wenzelm@23961
|
207 |
if self_critical () then e ()
|
wenzelm@23961
|
208 |
else
|
wenzelm@26083
|
209 |
uninterruptible (fn restore_attributes => fn () =>
|
wenzelm@24208
|
210 |
let
|
wenzelm@24208
|
211 |
val name' = ! critical_name;
|
wenzelm@24208
|
212 |
val _ =
|
wenzelm@24208
|
213 |
if Mutex.trylock critical_lock then ()
|
wenzelm@24208
|
214 |
else
|
wenzelm@24208
|
215 |
let
|
wenzelm@24208
|
216 |
val timer = Timer.startRealTimer ();
|
wenzelm@24208
|
217 |
val _ = tracing 4 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
|
wenzelm@24208
|
218 |
val _ = Mutex.lock critical_lock;
|
wenzelm@24208
|
219 |
val time = Timer.checkRealTimer timer;
|
wenzelm@24208
|
220 |
val _ = tracing (if Time.> (time, Time.fromMilliseconds 10) then 3 else 4) (fn () =>
|
wenzelm@24208
|
221 |
"CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
|
wenzelm@24208
|
222 |
in () end;
|
wenzelm@24208
|
223 |
val _ = critical_thread := SOME (Thread.self ());
|
wenzelm@24208
|
224 |
val _ = critical_name := name;
|
wenzelm@26083
|
225 |
val result = Exn.capture (restore_attributes e) ();
|
wenzelm@24208
|
226 |
val _ = critical_name := "";
|
wenzelm@24208
|
227 |
val _ = critical_thread := NONE;
|
wenzelm@24208
|
228 |
val _ = Mutex.unlock critical_lock;
|
wenzelm@24208
|
229 |
in Exn.release result end) ();
|
wenzelm@23961
|
230 |
|
wenzelm@23991
|
231 |
fun CRITICAL e = NAMED_CRITICAL "" e;
|
wenzelm@23981
|
232 |
|
wenzelm@23961
|
233 |
end;
|
wenzelm@23961
|
234 |
|
wenzelm@23973
|
235 |
|
wenzelm@24208
|
236 |
(* scheduling -- multiple threads working on a queue of tasks *)
|
wenzelm@24208
|
237 |
|
wenzelm@24208
|
238 |
datatype 'a task =
|
wenzelm@24208
|
239 |
Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
|
wenzelm@23973
|
240 |
|
wenzelm@26083
|
241 |
fun schedule n next_task = uninterruptible (fn restore_attributes => fn tasks =>
|
wenzelm@23973
|
242 |
let
|
wenzelm@23973
|
243 |
(*protected execution*)
|
wenzelm@23973
|
244 |
val lock = Mutex.mutex ();
|
wenzelm@24672
|
245 |
val protected_name = ref "";
|
wenzelm@24063
|
246 |
fun PROTECTED name e =
|
wenzelm@23973
|
247 |
let
|
wenzelm@24144
|
248 |
val name' = ! protected_name;
|
wenzelm@23981
|
249 |
val _ =
|
wenzelm@23981
|
250 |
if Mutex.trylock lock then ()
|
wenzelm@23981
|
251 |
else
|
wenzelm@24144
|
252 |
let
|
wenzelm@24144
|
253 |
val _ = tracing 2 (fn () => "PROTECTED" ^ show name ^ show' name' ^ ": waiting");
|
wenzelm@24144
|
254 |
val _ = Mutex.lock lock;
|
wenzelm@24144
|
255 |
val _ = tracing 2 (fn () => "PROTECTED" ^ show name ^ show' name' ^ ": passed");
|
wenzelm@24144
|
256 |
in () end;
|
wenzelm@24069
|
257 |
val _ = protected_name := name;
|
wenzelm@23973
|
258 |
val res = Exn.capture e ();
|
wenzelm@24069
|
259 |
val _ = protected_name := "";
|
wenzelm@23973
|
260 |
val _ = Mutex.unlock lock;
|
wenzelm@23973
|
261 |
in Exn.release res end;
|
wenzelm@23973
|
262 |
|
wenzelm@24072
|
263 |
(*wakeup condition*)
|
wenzelm@24072
|
264 |
val wakeup = ConditionVar.conditionVar ();
|
wenzelm@24072
|
265 |
fun wakeup_all () = ConditionVar.broadcast wakeup;
|
wenzelm@24072
|
266 |
fun wait () = ConditionVar.wait (wakeup, lock);
|
wenzelm@24291
|
267 |
fun wait_timeout () = ConditionVar.waitUntil (wakeup, lock, Time.now () + Time.fromSeconds 1);
|
wenzelm@24072
|
268 |
|
wenzelm@24214
|
269 |
(*queue of tasks*)
|
wenzelm@23973
|
270 |
val queue = ref tasks;
|
wenzelm@24072
|
271 |
val active = ref 0;
|
wenzelm@24119
|
272 |
fun trace_active () = tracing 1 (fn () => "SCHEDULE: " ^ Int.toString (! active) ^ " active");
|
wenzelm@24072
|
273 |
fun dequeue () =
|
wenzelm@23973
|
274 |
let
|
wenzelm@23981
|
275 |
val (next, tasks') = next_task (! queue);
|
wenzelm@23973
|
276 |
val _ = queue := tasks';
|
wenzelm@24072
|
277 |
in
|
wenzelm@24208
|
278 |
(case next of Wait =>
|
wenzelm@24208
|
279 |
(dec active; trace_active ();
|
wenzelm@24208
|
280 |
wait ();
|
wenzelm@24208
|
281 |
inc active; trace_active ();
|
wenzelm@24208
|
282 |
dequeue ())
|
wenzelm@24208
|
283 |
| _ => next)
|
wenzelm@24072
|
284 |
end;
|
wenzelm@23973
|
285 |
|
wenzelm@24208
|
286 |
(*pool of running threads*)
|
wenzelm@23973
|
287 |
val status = ref ([]: exn list);
|
wenzelm@24208
|
288 |
val running = ref ([]: Thread.thread list);
|
wenzelm@24208
|
289 |
fun start f =
|
wenzelm@24208
|
290 |
(inc active;
|
wenzelm@24208
|
291 |
change running (cons (Thread.fork (f, [Thread.InterruptState Thread.InterruptDefer]))));
|
wenzelm@24208
|
292 |
fun stop () =
|
wenzelm@24208
|
293 |
(dec active;
|
wenzelm@24208
|
294 |
change running (List.filter (fn t => not (Thread.equal (t, Thread.self ())))));
|
wenzelm@24208
|
295 |
|
wenzelm@24208
|
296 |
(*worker thread*)
|
wenzelm@24208
|
297 |
fun worker () =
|
wenzelm@24072
|
298 |
(case PROTECTED "dequeue" dequeue of
|
wenzelm@24208
|
299 |
Task {body, cont, fail} =>
|
wenzelm@26083
|
300 |
(case Exn.capture (restore_attributes body) () of
|
wenzelm@24208
|
301 |
Exn.Result () =>
|
wenzelm@24208
|
302 |
(PROTECTED "cont" (fn () => (change queue cont; wakeup_all ())); worker ())
|
wenzelm@23981
|
303 |
| Exn.Exn exn =>
|
wenzelm@24208
|
304 |
PROTECTED "fail" (fn () =>
|
wenzelm@24208
|
305 |
(change status (cons exn); change queue fail; stop (); wakeup_all ())))
|
wenzelm@24208
|
306 |
| Terminate => PROTECTED "terminate" (fn () => (stop (); wakeup_all ())));
|
wenzelm@23973
|
307 |
|
wenzelm@23973
|
308 |
(*main control: fork and wait*)
|
wenzelm@23973
|
309 |
fun fork 0 = ()
|
wenzelm@24208
|
310 |
| fork k = (start worker; fork (k - 1));
|
wenzelm@24063
|
311 |
val _ = PROTECTED "main" (fn () =>
|
wenzelm@24063
|
312 |
(fork (Int.max (n, 1));
|
wenzelm@24208
|
313 |
while not (List.null (! running)) do
|
wenzelm@24208
|
314 |
(trace_active ();
|
wenzelm@26254
|
315 |
if not (List.null (! status))
|
wenzelm@26254
|
316 |
then (List.app (fn t => Thread.interrupt t handle Thread _ => ()) (! running))
|
wenzelm@26254
|
317 |
else ();
|
wenzelm@24291
|
318 |
wait_timeout ())));
|
wenzelm@23973
|
319 |
|
wenzelm@24208
|
320 |
in ! status end);
|
wenzelm@23973
|
321 |
|
wenzelm@25704
|
322 |
|
wenzelm@25704
|
323 |
(* serial numbers *)
|
wenzelm@25704
|
324 |
|
wenzelm@25704
|
325 |
local
|
wenzelm@25704
|
326 |
|
wenzelm@25704
|
327 |
val serial_lock = Mutex.mutex ();
|
wenzelm@25704
|
328 |
val serial_count = ref 0;
|
wenzelm@25704
|
329 |
|
wenzelm@25704
|
330 |
in
|
wenzelm@25704
|
331 |
|
wenzelm@25704
|
332 |
val serial = uninterruptible (fn _ => fn () =>
|
wenzelm@25704
|
333 |
let
|
wenzelm@25704
|
334 |
val _ = Mutex.lock serial_lock;
|
wenzelm@25704
|
335 |
val res = inc serial_count;
|
wenzelm@25704
|
336 |
val _ = Mutex.unlock serial_lock;
|
wenzelm@25704
|
337 |
in res end);
|
wenzelm@25704
|
338 |
|
wenzelm@23961
|
339 |
end;
|
wenzelm@23961
|
340 |
|
wenzelm@25735
|
341 |
|
wenzelm@25735
|
342 |
(* thread data *)
|
wenzelm@25735
|
343 |
|
wenzelm@25735
|
344 |
val get_data = Thread.getLocal;
|
wenzelm@25735
|
345 |
val put_data = Thread.setLocal;
|
wenzelm@25735
|
346 |
|
wenzelm@25704
|
347 |
end;
|
wenzelm@24688
|
348 |
|
wenzelm@25704
|
349 |
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
|
wenzelm@25704
|
350 |
open BasicMultithreading;
|