--- a/src/Pure/ML-Systems/polyml-interrupt-timeout.ML Thu Nov 09 11:58:51 2006 +0100
+++ b/src/Pure/ML-Systems/polyml-interrupt-timeout.ML Thu Nov 09 16:14:43 2006 +0100
@@ -1,47 +1,26 @@
(* Title: Pure/ML-Systems/polyml-interrupt-timeout.ML
ID: $Id$
- Author: Tjark Weber, Makarius
+ Author: Tjark Weber
Copyright 2006
Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
*)
-(* FIXME: this code appears to disable signal handling in child databases altogether (?)
-local
-
- val alarm_active = ref false;
-
- val _ = Signal.signal (Posix.Signal.alrm, Signal.SIG_HANDLE (fn _ =>
- let val active = ! alarm_active in
- alarm_active := false;
- if active then
- Process.interruptConsoleProcesses ()
- else
- ()
- end));
-
-in
+(* Note: This code may cause an infrequent segmentation fault (due to a race
+ condition between process creation/termination and garbage collection)
+ before PolyML 5.0. *)
- fun interrupt_timeout time f x =
- let
- fun deactivate_alarm () = (
- alarm_active := false;
- Posix.Process.alarm Time.zeroTime
- )
- in
- alarm_active := true;
- Posix.Process.alarm time;
- let val result = f x in
- deactivate_alarm ();
- result
- end handle exn => (
- deactivate_alarm ();
- raise exn
- )
- end;
-
-end;
-*)
+(* Note: f must not manipulate the timer used by Posix.Process.sleep *)
fun interrupt_timeout time f x =
- f x;
+let
+ val ch = Process.channel ()
+ val interrupt_timer = Process.console (fn () =>
+ (Posix.Process.sleep time; Process.send (ch, NONE)))
+ val interrupt_worker = Process.console (fn () =>
+ Process.send (ch, SOME (capture f x)))
+in
+ case Process.receive ch of
+ NONE => (interrupt_worker (); raise Interrupt)
+ | SOME fx => (interrupt_timer (); release fx)
+end;