13 structure TimeLimit: TIME_LIMIT = |
13 structure TimeLimit: TIME_LIMIT = |
14 struct |
14 struct |
15 |
15 |
16 exception TimeOut; |
16 exception TimeOut; |
17 |
17 |
18 fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () => |
18 fun timeLimit time f x = |
19 let |
19 Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts => |
20 val worker = Thread.self (); |
20 let |
21 val timeout = Unsynchronized.ref false; |
21 val main = Thread.self (); |
22 val watchdog = Thread.fork (fn () => |
22 val timeout = Unsynchronized.ref false; |
23 (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []); |
23 val watchdog = Simple_Thread.fork true (fn () => |
|
24 (OS.Process.sleep time; timeout := true; Thread.interrupt main)); |
24 |
25 |
25 val result = Exn.capture (restore_attributes f) x; |
26 val result = Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) (); |
26 val was_timeout = Exn.is_interrupt_exn result andalso ! timeout; |
|
27 |
27 |
28 val _ = Thread.interrupt watchdog handle Thread _ => (); |
28 val _ = Thread.interrupt watchdog handle Thread _ => (); |
29 in if was_timeout then raise TimeOut else Exn.release result end) (); |
29 val _ = while Thread.isActive watchdog do OS.Process.sleep (seconds 0.0001); |
|
30 |
|
31 val test = |
|
32 Exn.capture (fn () => |
|
33 Multithreading.with_attributes (Multithreading.sync_interrupts orig_atts) |
|
34 (fn _ => Thread.testInterrupt ())) (); |
|
35 in |
|
36 if ! timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test) |
|
37 then raise TimeOut |
|
38 else if Exn.is_interrupt_exn test then Exn.interrupt () |
|
39 else Exn.release result |
|
40 end); |
30 |
41 |
31 end; |
42 end; |
32 |
43 |