1 (* Title: Pure/ML-Systems/polyml-interrupt-timeout.ML |
1 (* Title: Pure/ML-Systems/polyml-interrupt-timeout.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tjark Weber, Makarius |
3 Author: Tjark Weber |
4 Copyright 2006 |
4 Copyright 2006 |
5 |
5 |
6 Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML. |
6 Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML. |
7 *) |
7 *) |
8 |
8 |
9 (* FIXME: this code appears to disable signal handling in child databases altogether (?) |
9 (* Note: This code may cause an infrequent segmentation fault (due to a race |
10 local |
10 condition between process creation/termination and garbage collection) |
|
11 before PolyML 5.0. *) |
11 |
12 |
12 val alarm_active = ref false; |
13 (* Note: f must not manipulate the timer used by Posix.Process.sleep *) |
13 |
|
14 val _ = Signal.signal (Posix.Signal.alrm, Signal.SIG_HANDLE (fn _ => |
|
15 let val active = ! alarm_active in |
|
16 alarm_active := false; |
|
17 if active then |
|
18 Process.interruptConsoleProcesses () |
|
19 else |
|
20 () |
|
21 end)); |
|
22 |
|
23 in |
|
24 |
|
25 fun interrupt_timeout time f x = |
|
26 let |
|
27 fun deactivate_alarm () = ( |
|
28 alarm_active := false; |
|
29 Posix.Process.alarm Time.zeroTime |
|
30 ) |
|
31 in |
|
32 alarm_active := true; |
|
33 Posix.Process.alarm time; |
|
34 let val result = f x in |
|
35 deactivate_alarm (); |
|
36 result |
|
37 end handle exn => ( |
|
38 deactivate_alarm (); |
|
39 raise exn |
|
40 ) |
|
41 end; |
|
42 |
|
43 end; |
|
44 *) |
|
45 |
14 |
46 fun interrupt_timeout time f x = |
15 fun interrupt_timeout time f x = |
47 f x; |
16 let |
|
17 val ch = Process.channel () |
|
18 val interrupt_timer = Process.console (fn () => |
|
19 (Posix.Process.sleep time; Process.send (ch, NONE))) |
|
20 val interrupt_worker = Process.console (fn () => |
|
21 Process.send (ch, SOME (capture f x))) |
|
22 in |
|
23 case Process.receive ch of |
|
24 NONE => (interrupt_worker (); raise Interrupt) |
|
25 | SOME fx => (interrupt_timer (); release fx) |
|
26 end; |