10 signature MULTITHREADING = |
10 signature MULTITHREADING = |
11 sig |
11 sig |
12 include MULTITHREADING |
12 include MULTITHREADING |
13 val ignore_interrupt: ('a -> 'b) -> 'a -> 'b |
13 val ignore_interrupt: ('a -> 'b) -> 'a -> 'b |
14 val raise_interrupt: ('a -> 'b) -> 'a -> 'b |
14 val raise_interrupt: ('a -> 'b) -> 'a -> 'b |
15 val interrupt_timeout: Time.time -> ('a -> 'b) -> 'a -> 'b |
15 structure TimeLimit: TIME_LIMIT |
16 end; |
16 end; |
17 |
17 |
18 structure Multithreading: MULTITHREADING = |
18 structure Multithreading: MULTITHREADING = |
19 struct |
19 struct |
20 |
20 |
70 [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce] f x; |
70 [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce] f x; |
71 |
71 |
72 fun ignore_interrupt f = uninterruptible (fn _ => f); |
72 fun ignore_interrupt f = uninterruptible (fn _ => f); |
73 fun raise_interrupt f = interruptible (fn _ => f); |
73 fun raise_interrupt f = interruptible (fn _ => f); |
74 |
74 |
75 fun interrupt_timeout time f x = |
75 |
|
76 (* execution with time limit *) |
|
77 |
|
78 structure TimeLimit = |
|
79 struct |
|
80 |
|
81 exception TimeOut; |
|
82 |
|
83 fun timeLimit time f x = |
76 uninterruptible (fn atts => fn () => |
84 uninterruptible (fn atts => fn () => |
77 let |
85 let |
78 val worker = Thread.self (); |
86 val worker = Thread.self (); |
|
87 val timeout = ref false; |
79 val watchdog = Thread.fork (interruptible (fn _ => fn () => |
88 val watchdog = Thread.fork (interruptible (fn _ => fn () => |
80 (OS.Process.sleep time; Thread.interrupt worker)), []); |
89 (OS.Process.sleep time; timeout := true; Thread.interrupt worker)), []); |
|
90 |
|
91 (*RACE! timeout signal vs. external Interrupt*) |
81 val result = Exn.capture (with_attributes atts (fn _ => f)) x; |
92 val result = Exn.capture (with_attributes atts (fn _ => f)) x; |
|
93 val was_timeout = (case result of Exn.Exn Interrupt => ! timeout | _ => false); |
|
94 |
82 val _ = Thread.interrupt watchdog handle Thread _ => (); |
95 val _ = Thread.interrupt watchdog handle Thread _ => (); |
83 in Exn.release result end) (); |
96 in if was_timeout then raise TimeOut else Exn.release result end) (); |
|
97 |
|
98 end; |
84 |
99 |
85 |
100 |
86 (* critical section -- may be nested within the same thread *) |
101 (* critical section -- may be nested within the same thread *) |
87 |
102 |
88 local |
103 local |
214 |
229 |
215 end; |
230 end; |
216 |
231 |
217 val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL; |
232 val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL; |
218 val CRITICAL = Multithreading.CRITICAL; |
233 val CRITICAL = Multithreading.CRITICAL; |
|
234 |
219 val ignore_interrupt = Multithreading.ignore_interrupt; |
235 val ignore_interrupt = Multithreading.ignore_interrupt; |
220 val raise_interrupt = Multithreading.raise_interrupt; |
236 val raise_interrupt = Multithreading.raise_interrupt; |
221 val interrupt_timeout = Multithreading.interrupt_timeout; |
237 |
222 |
238 structure TimeLimit = Multithreading.TimeLimit; |
|
239 |