equal
deleted
inserted
replaced
|
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; |