src/Pure/ML-Systems/multithreading_polyml.ML
changeset 24688 a5754ca5c510
parent 24672 f311717d1f03
child 25704 df9c8074ff09
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Sep 23 23:39:42 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 24 13:52:50 2007 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    include MULTITHREADING
     1.5    val ignore_interrupt: ('a -> 'b) -> 'a -> 'b
     1.6    val raise_interrupt: ('a -> 'b) -> 'a -> 'b
     1.7 -  val interrupt_timeout: Time.time -> ('a -> 'b) -> 'a -> 'b
     1.8 +  structure TimeLimit: TIME_LIMIT
     1.9  end;
    1.10  
    1.11  structure Multithreading: MULTITHREADING =
    1.12 @@ -72,15 +72,30 @@
    1.13  fun ignore_interrupt f = uninterruptible (fn _ => f);
    1.14  fun raise_interrupt f = interruptible (fn _ => f);
    1.15  
    1.16 -fun interrupt_timeout time f x =
    1.17 +
    1.18 +(* execution with time limit *)
    1.19 +
    1.20 +structure TimeLimit =
    1.21 +struct
    1.22 +
    1.23 +exception TimeOut;
    1.24 +
    1.25 +fun timeLimit time f x =
    1.26    uninterruptible (fn atts => fn () =>
    1.27      let
    1.28        val worker = Thread.self ();
    1.29 +      val timeout = ref false;
    1.30        val watchdog = Thread.fork (interruptible (fn _ => fn () =>
    1.31 -        (OS.Process.sleep time; Thread.interrupt worker)), []);
    1.32 +        (OS.Process.sleep time; timeout := true; Thread.interrupt worker)), []);
    1.33 +
    1.34 +      (*RACE! timeout signal vs. external Interrupt*)
    1.35        val result = Exn.capture (with_attributes atts (fn _ => f)) x;
    1.36 +      val was_timeout = (case result of Exn.Exn Interrupt => ! timeout | _ => false);
    1.37 +
    1.38        val _ = Thread.interrupt watchdog handle Thread _ => ();
    1.39 -    in Exn.release result end) ();
    1.40 +    in if was_timeout then raise TimeOut else Exn.release result end) ();
    1.41 +
    1.42 +end;
    1.43  
    1.44  
    1.45  (* critical section -- may be nested within the same thread *)
    1.46 @@ -216,7 +231,9 @@
    1.47  
    1.48  val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
    1.49  val CRITICAL = Multithreading.CRITICAL;
    1.50 +
    1.51  val ignore_interrupt = Multithreading.ignore_interrupt;
    1.52  val raise_interrupt = Multithreading.raise_interrupt;
    1.53 -val interrupt_timeout = Multithreading.interrupt_timeout;
    1.54  
    1.55 +structure TimeLimit = Multithreading.TimeLimit;
    1.56 +