replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
authorwenzelm
Mon Sep 24 13:52:50 2007 +0200 (2007-09-24 ago)
changeset 24688a5754ca5c510
parent 24687 f24306b9e073
child 24689 ac5b5a6155dd
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
src/HOL/Tools/refute.ML
src/Pure/ML-Systems/alice.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ML-Systems/polyml-interrupt-timeout.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/poplogml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML-Systems/time_limit.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Sun Sep 23 23:39:42 2007 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Sep 24 13:52:50 2007 +0200
     1.3 @@ -1240,9 +1240,9 @@
     1.4          ^ (if negate then "refutes" else "satisfies") ^ ": "
     1.5          ^ Sign.string_of_term thy t);
     1.6        if maxtime>0 then (
     1.7 -        interrupt_timeout (Time.fromSeconds (Int.toLarge maxtime))
     1.8 +        TimeLimit.timeLimit (Time.fromSeconds maxtime)
     1.9            wrapper ()
    1.10 -        handle Interrupt =>
    1.11 +        handle TimeLimit.TimeOut =>
    1.12            writeln ("\nSearch terminated, time limit (" ^ string_of_int maxtime
    1.13              ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.")
    1.14        ) else
     2.1 --- a/src/Pure/ML-Systems/alice.ML	Sun Sep 23 23:39:42 2007 +0200
     2.2 +++ b/src/Pure/ML-Systems/alice.ML	Mon Sep 24 13:52:50 2007 +0200
     2.3 @@ -16,7 +16,8 @@
     2.4  val ml_system_fix_ints = false;
     2.5  
     2.6  use "ML-Systems/exn.ML";
     2.7 -use "ML-Systems/multithreading_dummy.ML";
     2.8 +use "ML-Systems/multithreading.ML";
     2.9 +use "ML-Systems/time_limit.ML";
    2.10  
    2.11  
    2.12  fun exit 0 = (OS.Process.exit OS.Process.success): unit
    2.13 @@ -125,13 +126,6 @@
    2.14  end;
    2.15  
    2.16  
    2.17 -(* bounded time execution *)
    2.18 -
    2.19 -(*dummy implementation*)
    2.20 -fun interrupt_timeout time f x =
    2.21 -  f x;
    2.22 -
    2.23 -
    2.24  
    2.25  (** OS related **)
    2.26  
     3.1 --- a/src/Pure/ML-Systems/mosml.ML	Sun Sep 23 23:39:42 2007 +0200
     3.2 +++ b/src/Pure/ML-Systems/mosml.ML	Mon Sep 24 13:52:50 2007 +0200
     3.3 @@ -32,7 +32,8 @@
     3.4  load "IO";
     3.5  
     3.6  use "ML-Systems/exn.ML";
     3.7 -use "ML-Systems/multithreading_dummy.ML";
     3.8 +use "ML-Systems/multithreading.ML";
     3.9 +use "ML-Systems/time_limit.ML";
    3.10  
    3.11  
    3.12  (*low-level pointer equality*)
    3.13 @@ -141,13 +142,6 @@
    3.14  end;
    3.15  
    3.16  
    3.17 -(* bounded time execution *)
    3.18 -
    3.19 -(*dummy implementation*)
    3.20 -fun interrupt_timeout time f x =
    3.21 -  f x;
    3.22 -
    3.23 -
    3.24  (* ML command execution *)
    3.25  
    3.26  (*Can one redirect 'use' directly to an instream?*)
     4.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Sep 23 23:39:42 2007 +0200
     4.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 24 13:52:50 2007 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4    include MULTITHREADING
     4.5    val ignore_interrupt: ('a -> 'b) -> 'a -> 'b
     4.6    val raise_interrupt: ('a -> 'b) -> 'a -> 'b
     4.7 -  val interrupt_timeout: Time.time -> ('a -> 'b) -> 'a -> 'b
     4.8 +  structure TimeLimit: TIME_LIMIT
     4.9  end;
    4.10  
    4.11  structure Multithreading: MULTITHREADING =
    4.12 @@ -72,15 +72,30 @@
    4.13  fun ignore_interrupt f = uninterruptible (fn _ => f);
    4.14  fun raise_interrupt f = interruptible (fn _ => f);
    4.15  
    4.16 -fun interrupt_timeout time f x =
    4.17 +
    4.18 +(* execution with time limit *)
    4.19 +
    4.20 +structure TimeLimit =
    4.21 +struct
    4.22 +
    4.23 +exception TimeOut;
    4.24 +
    4.25 +fun timeLimit time f x =
    4.26    uninterruptible (fn atts => fn () =>
    4.27      let
    4.28        val worker = Thread.self ();
    4.29 +      val timeout = ref false;
    4.30        val watchdog = Thread.fork (interruptible (fn _ => fn () =>
    4.31 -        (OS.Process.sleep time; Thread.interrupt worker)), []);
    4.32 +        (OS.Process.sleep time; timeout := true; Thread.interrupt worker)), []);
    4.33 +
    4.34 +      (*RACE! timeout signal vs. external Interrupt*)
    4.35        val result = Exn.capture (with_attributes atts (fn _ => f)) x;
    4.36 +      val was_timeout = (case result of Exn.Exn Interrupt => ! timeout | _ => false);
    4.37 +
    4.38        val _ = Thread.interrupt watchdog handle Thread _ => ();
    4.39 -    in Exn.release result end) ();
    4.40 +    in if was_timeout then raise TimeOut else Exn.release result end) ();
    4.41 +
    4.42 +end;
    4.43  
    4.44  
    4.45  (* critical section -- may be nested within the same thread *)
    4.46 @@ -216,7 +231,9 @@
    4.47  
    4.48  val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
    4.49  val CRITICAL = Multithreading.CRITICAL;
    4.50 +
    4.51  val ignore_interrupt = Multithreading.ignore_interrupt;
    4.52  val raise_interrupt = Multithreading.raise_interrupt;
    4.53 -val interrupt_timeout = Multithreading.interrupt_timeout;
    4.54  
    4.55 +structure TimeLimit = Multithreading.TimeLimit;
    4.56 +
     5.1 --- a/src/Pure/ML-Systems/polyml-interrupt-timeout.ML	Sun Sep 23 23:39:42 2007 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,35 +0,0 @@
     5.4 -(*  Title:      Pure/ML-Systems/polyml-interrupt-timeout.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Tjark Weber
     5.7 -    Copyright   2006-2007
     5.8 -
     5.9 -Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
    5.10 -*)
    5.11 -
    5.12 -(* Note: This code may cause an infrequent segmentation fault (due to a race
    5.13 -         condition between process creation/termination and garbage collection)
    5.14 -         before PolyML 5.0. *)
    5.15 -
    5.16 -(* Note: The timer process sometimes does not receive enough CPU time to put
    5.17 -         itself to sleep.  It then cannot indicate a timeout when (or soon
    5.18 -         after) the specified time has elapsed.  This issue is obviously caused
    5.19 -         by the process scheduling algorithm in current PolyML versions.  We
    5.20 -         could use additional communication between the timer and the worker
    5.21 -         process to ensure that the timer receives /some/ CPU time, but there
    5.22 -         seems to be no way to guarantee that the timer process receives
    5.23 -         sufficient CPU time to complete its task. *)
    5.24 -
    5.25 -(* Note: f must not manipulate the timer used by Posix.Process.sleep *)
    5.26 -
    5.27 -fun interrupt_timeout time f x =
    5.28 -let
    5.29 -  val ch = Process.channel ()
    5.30 -  val interrupt_timer = Process.console (fn () =>
    5.31 -    (Posix.Process.sleep time; Process.send (ch, NONE)))
    5.32 -  val interrupt_worker = Process.console (fn () =>
    5.33 -    Process.send (ch, SOME (Exn.capture f x)))
    5.34 -in
    5.35 -  case Process.receive ch of
    5.36 -    NONE    => (interrupt_worker (); raise Interrupt)
    5.37 -  | SOME fx => (interrupt_timer (); Exn.release fx)
    5.38 -end;
     6.1 --- a/src/Pure/ML-Systems/polyml.ML	Sun Sep 23 23:39:42 2007 +0200
     6.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Sep 24 13:52:50 2007 +0200
     6.3 @@ -5,7 +5,8 @@
     6.4  *)
     6.5  
     6.6  use "ML-Systems/exn.ML";
     6.7 -use "ML-Systems/multithreading_dummy.ML";
     6.8 +use "ML-Systems/multithreading.ML";
     6.9 +use "ML-Systems/time_limit.ML";
    6.10  
    6.11  val ml_system_fix_ints = false;
    6.12  
    6.13 @@ -60,13 +61,6 @@
    6.14    in (sys, usr, gc) end;
    6.15  
    6.16  
    6.17 -(* bounded time execution *)
    6.18 -
    6.19 -(*dummy implementation*)
    6.20 -fun interrupt_timeout time f x =
    6.21 -  f x;
    6.22 -
    6.23 -
    6.24  (* prompts *)
    6.25  
    6.26  fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
     7.1 --- a/src/Pure/ML-Systems/poplogml.ML	Sun Sep 23 23:39:42 2007 +0200
     7.2 +++ b/src/Pure/ML-Systems/poplogml.ML	Mon Sep 24 13:52:50 2007 +0200
     7.3 @@ -272,12 +272,6 @@
     7.4  end;
     7.5  
     7.6  
     7.7 -(* bounded time execution *)
     7.8 -
     7.9 -(* FIXME proper implementation available? *)
    7.10 -fun interrupt_timeout time f x =
    7.11 -  f x;
    7.12 -
    7.13  
    7.14  (** interrupts **)      (*Note: may get into race conditions*)
    7.15  
     8.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sun Sep 23 23:39:42 2007 +0200
     8.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Sep 24 13:52:50 2007 +0200
     8.3 @@ -7,7 +7,7 @@
     8.4  use "ML-Systems/proper_int.ML";
     8.5  use "ML-Systems/overloading_smlnj.ML";
     8.6  use "ML-Systems/exn.ML";
     8.7 -use "ML-Systems/multithreading_dummy.ML";
     8.8 +use "ML-Systems/multithreading.ML";
     8.9  
    8.10  
    8.11  (*low-level pointer equality*)
    8.12 @@ -169,13 +169,6 @@
    8.13  end;
    8.14  
    8.15  
    8.16 -(* bounded time execution *)
    8.17 -
    8.18 -fun interrupt_timeout time f x =
    8.19 -  TimeLimit.timeLimit time f x
    8.20 -    handle TimeLimit.TimeOut => raise Interrupt;
    8.21 -
    8.22 -
    8.23  (** Signal handling: emulation of the Poly/ML Signal structure. Note that types
    8.24      Posix.Signal.signal and Signals.signal differ **)
    8.25  
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Pure/ML-Systems/time_limit.ML	Mon Sep 24 13:52:50 2007 +0200
     9.3 @@ -0,0 +1,21 @@
     9.4 +(*  Title:      Pure/ML-Systems/time_limit.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:     Makarius
     9.7 +
     9.8 +Dummy implementation of NJ's TimeLimit structure.
     9.9 +*)
    9.10 +
    9.11 +signature TIME_LIMIT =
    9.12 +sig
    9.13 +  exception TimeOut
    9.14 +  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
    9.15 +end;
    9.16 +
    9.17 +structure TimeLimit: TIME_LIMIT =
    9.18 +struct
    9.19 +
    9.20 +exception TimeOut;
    9.21 +fun timeLimit _ f x = f x;
    9.22 +
    9.23 +end;
    9.24 +
    10.1 --- a/src/Pure/codegen.ML	Sun Sep 23 23:39:42 2007 +0200
    10.2 +++ b/src/Pure/codegen.ML	Mon Sep 24 13:52:50 2007 +0200
    10.3 @@ -996,14 +996,14 @@
    10.4    in
    10.5      if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
    10.6      then
    10.7 -      (case try (fn state => interrupt_timeout (!auto_quickcheck_time_limit)
    10.8 +      (case try (fn state => TimeLimit.timeLimit (!auto_quickcheck_time_limit)
    10.9             (test_goal true (params, []) 1 assms) state) state of
   10.10           SOME (cex as SOME _) =>
   10.11             Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
   10.12               Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
   10.13         | _ => state)
   10.14      else state
   10.15 -  end handle Interrupt => state;
   10.16 +  end handle TimeLimit.TimeOut => state;
   10.17  
   10.18  val _ = Context.add_setup
   10.19    (Context.theory_map (Specification.add_theorem_hook test_goal'));