On Fri, 1 Aug 2008, Mike Gordon wrote:
> Does anyone know if it is possible to run a function (e.g. SIMP_CONV
> arith_ss []) for a fixed time and then fail on timeout. I vaguely
> remember that there was no way to do this, but want to double check.
This is reasonably easy in recent versions of Poly/ML (5.1 or 5.2), thanks
to support for (native) Posix threads. The basic idea is to have a
watchdog interrupt the current worker after some time:
structure TimeLimit =
struct
exception TimeOut;
fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
let
val worker = Thread.self ();
val timeout = ref false;
val watchdog = Thread.fork (fn () =>
(OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
(*RACE! timeout signal vs. external Interrupt*)
val result = Exn.capture (restore_attributes f) x;
val was_timeout = (case result of Exn.Exn Interrupt => ! timeout | _ =>
false);
val _ = Thread.interrupt watchdog handle Thread _ => ();
in if was_timeout then raise TimeOut else Exn.release result end) ();
end;
The interface emulates the TimeLimit structure of SML/NJ, even though that
platform is no longer used seriously.
See also the first part of
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2008/src/Pure/ML-Systems/multithreading_polyml.ML
for the actual source, including some of our auxiliary combinators for
changing thread attributes (interrruptibility etc.).
Makarius
-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
