equal
deleted
inserted
replaced
10 structure Multithreading: MULTITHREADING = |
10 structure Multithreading: MULTITHREADING = |
11 struct |
11 struct |
12 |
12 |
13 (* options *) |
13 (* options *) |
14 |
14 |
15 val trace = ref false; |
15 val trace = ref 0; |
16 fun tracing msg = |
16 fun tracing level msg = |
17 if ! trace |
17 if level <= ! trace |
18 then (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr) |
18 then (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr) |
19 else (); |
19 else (); |
20 |
20 |
21 val available = true; |
21 val available = true; |
22 val max_threads = ref 1; |
22 val max_threads = ref 1; |
56 val _ = |
56 val _ = |
57 if Mutex.trylock critical_lock then () |
57 if Mutex.trylock critical_lock then () |
58 else |
58 else |
59 let |
59 let |
60 val timer = Timer.startRealTimer (); |
60 val timer = Timer.startRealTimer (); |
61 val _ = tracing (fn () => |
61 val _ = tracing 3 (fn () => |
62 "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": waiting"); |
62 "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": waiting"); |
63 val _ = Mutex.lock critical_lock; |
63 val _ = Mutex.lock critical_lock; |
64 val _ = tracing (fn () => |
64 val _ = tracing 3 (fn () => |
65 "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": passed after " ^ |
65 "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": passed after " ^ |
66 Time.toString (Timer.checkRealTimer timer)); |
66 Time.toString (Timer.checkRealTimer timer)); |
67 in () end; |
67 in () end; |
68 val _ = critical_thread := SOME (Thread.self ()); |
68 val _ = critical_thread := SOME (Thread.self ()); |
69 val _ = critical_name := name; |
69 val _ = critical_name := name; |
93 fun PROTECTED name e = |
93 fun PROTECTED name e = |
94 let |
94 let |
95 val _ = |
95 val _ = |
96 if Mutex.trylock lock then () |
96 if Mutex.trylock lock then () |
97 else |
97 else |
98 (tracing (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": waiting"); |
98 (tracing 2 (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": waiting"); |
99 Mutex.lock lock; |
99 Mutex.lock lock; |
100 tracing (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": passed")); |
100 tracing 2 (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": passed")); |
101 val _ = protected_name := name; |
101 val _ = protected_name := name; |
102 val res = Exn.capture e (); |
102 val res = Exn.capture e (); |
103 val _ = protected_name := ""; |
103 val _ = protected_name := ""; |
104 val _ = Mutex.unlock lock; |
104 val _ = Mutex.unlock lock; |
105 in Exn.release res end; |
105 in Exn.release res end; |
110 fun wait () = ConditionVar.wait (wakeup, lock); |
110 fun wait () = ConditionVar.wait (wakeup, lock); |
111 |
111 |
112 (*the queue of tasks*) |
112 (*the queue of tasks*) |
113 val queue = ref tasks; |
113 val queue = ref tasks; |
114 val active = ref 0; |
114 val active = ref 0; |
115 fun trace_active () = tracing (fn () => "SCHEDULE: " ^ Int.toString (! active) ^ " active"); |
115 fun trace_active () = tracing 1 (fn () => "SCHEDULE: " ^ Int.toString (! active) ^ " active"); |
116 fun dequeue () = |
116 fun dequeue () = |
117 let |
117 let |
118 val (next, tasks') = next_task (! queue); |
118 val (next, tasks') = next_task (! queue); |
119 val _ = queue := tasks'; |
119 val _ = queue := tasks'; |
120 in |
120 in |