23961
|
1 |
(* Title: Pure/ML-Systems/multithreading_polyml.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius
|
|
4 |
|
|
5 |
Multithreading in Poly/ML (version 5.1).
|
|
6 |
*)
|
|
7 |
|
|
8 |
open Thread;
|
|
9 |
|
|
10 |
structure Multithreading: MULTITHREADING =
|
|
11 |
struct
|
|
12 |
|
|
13 |
val number_of_threads = ref 0;
|
|
14 |
|
|
15 |
|
|
16 |
(* FIXME tmp *)
|
|
17 |
fun message s =
|
|
18 |
(TextIO.output (TextIO.stdErr, (">>> " ^ s ^ "\n")); TextIO.flushOut TextIO.stdErr);
|
|
19 |
|
|
20 |
|
|
21 |
(* critical section -- may be nested within the same thread *)
|
|
22 |
|
|
23 |
local
|
|
24 |
|
|
25 |
val critical_lock = Mutex.mutex ();
|
|
26 |
val critical_thread = ref (NONE: Thread.thread option);
|
|
27 |
|
|
28 |
in
|
|
29 |
|
|
30 |
fun self_critical () =
|
|
31 |
(case ! critical_thread of
|
|
32 |
NONE => false
|
|
33 |
| SOME id => Thread.equal (id, Thread.self ()));
|
|
34 |
|
|
35 |
fun CRITICAL e =
|
|
36 |
if self_critical () then e ()
|
|
37 |
else
|
|
38 |
let
|
|
39 |
val _ =
|
|
40 |
if Mutex.trylock critical_lock then ()
|
|
41 |
else
|
|
42 |
(message "Waiting for critical lock";
|
|
43 |
Mutex.lock critical_lock;
|
|
44 |
message "Obtained critical lock");
|
|
45 |
val _ = critical_thread := SOME (Thread.self ());
|
|
46 |
val result = Exn.capture e ();
|
|
47 |
val _ = critical_thread := NONE;
|
|
48 |
val _ = Mutex.unlock critical_lock;
|
|
49 |
in Exn.release result end;
|
|
50 |
|
|
51 |
end;
|
|
52 |
|
|
53 |
end;
|
|
54 |
|
|
55 |
val CRITICAL = Multithreading.CRITICAL;
|