51 |
51 |
52 fun NAMED_CRITICAL name e = |
52 fun NAMED_CRITICAL name e = |
53 if self_critical () then e () |
53 if self_critical () then e () |
54 else |
54 else |
55 let |
55 let |
|
56 val name' = ! critical_name; |
56 val _ = |
57 val _ = |
57 if Mutex.trylock critical_lock then () |
58 if Mutex.trylock critical_lock then () |
58 else |
59 else |
59 let |
60 let |
60 val timer = Timer.startRealTimer (); |
61 val timer = Timer.startRealTimer (); |
61 val _ = tracing 3 (fn () => |
62 val _ = tracing 4 (fn () => "CRITICAL" ^ show name ^ show' 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 3 (fn () => |
64 val time = Timer.checkRealTimer timer; |
65 "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": passed after " ^ |
65 val _ = tracing (if Time.> (time, Time.fromMilliseconds 10) then 3 else 4) (fn () => |
66 Time.toString (Timer.checkRealTimer timer)); |
66 "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time); |
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; |
70 val result = Exn.capture e (); |
70 val result = Exn.capture e (); |
71 val _ = critical_name := ""; |
71 val _ = critical_name := ""; |
90 let |
90 let |
91 (*protected execution*) |
91 (*protected execution*) |
92 val lock = Mutex.mutex (); |
92 val lock = Mutex.mutex (); |
93 fun PROTECTED name e = |
93 fun PROTECTED name e = |
94 let |
94 let |
|
95 val name' = ! protected_name; |
95 val _ = |
96 val _ = |
96 if Mutex.trylock lock then () |
97 if Mutex.trylock lock then () |
97 else |
98 else |
98 (tracing 2 (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": waiting"); |
99 let |
99 Mutex.lock lock; |
100 val _ = tracing 2 (fn () => "PROTECTED" ^ show name ^ show' name' ^ ": waiting"); |
100 tracing 2 (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": passed")); |
101 val _ = Mutex.lock lock; |
|
102 val _ = tracing 2 (fn () => "PROTECTED" ^ show name ^ show' name' ^ ": passed"); |
|
103 in () end; |
101 val _ = protected_name := name; |
104 val _ = protected_name := name; |
102 val res = Exn.capture e (); |
105 val res = Exn.capture e (); |
103 val _ = protected_name := ""; |
106 val _ = protected_name := ""; |
104 val _ = Mutex.unlock lock; |
107 val _ = Mutex.unlock lock; |
105 in Exn.release res end; |
108 in Exn.release res end; |