src/Pure/Concurrent/time_limit.ML
author hoelzl
Wed, 02 Apr 2014 18:35:01 +0200
changeset 56369 2704ca85be98
parent 52085 5534ec8b90a9
child 61182 9d0834562a78
permissions -rw-r--r--
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41710
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/time_limit.ML
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
     3
52051
9362fcd0318c modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents: 44112
diff changeset
     4
Execution with time limit (relative timeout).
41710
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
     5
*)
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
     6
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
     7
signature TIME_LIMIT =
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
     8
sig
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
     9
  exception TimeOut
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
    10
  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
    11
end;
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
    12
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
    13
structure TimeLimit: TIME_LIMIT =
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
    14
struct
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
    15
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
    16
exception TimeOut;
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
    17
52051
9362fcd0318c modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents: 44112
diff changeset
    18
fun timeLimit timeout f x =
41712
82339c3fd74a more robust TimeLimit: make double sure that watchdog has terminated and interrupts received during uninterruptible state are propagated (NB: Thread.testInterrupt requires InterruptSynch in Poly/ML 5.4.0 or earlier);
wenzelm
parents: 41710
diff changeset
    19
  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
82339c3fd74a more robust TimeLimit: make double sure that watchdog has terminated and interrupts received during uninterruptible state are propagated (NB: Thread.testInterrupt requires InterruptSynch in Poly/ML 5.4.0 or earlier);
wenzelm
parents: 41710
diff changeset
    20
    let
52051
9362fcd0318c modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents: 44112
diff changeset
    21
      val self = Thread.self ();
9362fcd0318c modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents: 44112
diff changeset
    22
9362fcd0318c modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents: 44112
diff changeset
    23
      val request =
9362fcd0318c modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents: 44112
diff changeset
    24
        Event_Timer.request (Time.+ (Time.now (), timeout))
9362fcd0318c modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents: 44112
diff changeset
    25
          (fn () => Simple_Thread.interrupt_unsynchronized self);
41712
82339c3fd74a more robust TimeLimit: make double sure that watchdog has terminated and interrupts received during uninterruptible state are propagated (NB: Thread.testInterrupt requires InterruptSynch in Poly/ML 5.4.0 or earlier);
wenzelm
parents: 41710
diff changeset
    26
41714
3bafa8ba51db always test/clear Multithreading.interrupted, indepently of thread attributes;
wenzelm
parents: 41712
diff changeset
    27
      val result =
3bafa8ba51db always test/clear Multithreading.interrupted, indepently of thread attributes;
wenzelm
parents: 41712
diff changeset
    28
        Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
41710
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
    29
52051
9362fcd0318c modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents: 44112
diff changeset
    30
      val was_timeout = not (Event_Timer.cancel request);
52064
4b4ff1d3b723 back to more paranoid interrupt test after request is cancelled -- avoid race condition;
wenzelm
parents: 52051
diff changeset
    31
      val test = Exn.capture Multithreading.interrupted ();
41712
82339c3fd74a more robust TimeLimit: make double sure that watchdog has terminated and interrupts received during uninterruptible state are propagated (NB: Thread.testInterrupt requires InterruptSynch in Poly/ML 5.4.0 or earlier);
wenzelm
parents: 41710
diff changeset
    32
    in
52064
4b4ff1d3b723 back to more paranoid interrupt test after request is cancelled -- avoid race condition;
wenzelm
parents: 52051
diff changeset
    33
      if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
41712
82339c3fd74a more robust TimeLimit: make double sure that watchdog has terminated and interrupts received during uninterruptible state are propagated (NB: Thread.testInterrupt requires InterruptSynch in Poly/ML 5.4.0 or earlier);
wenzelm
parents: 41710
diff changeset
    34
      then raise TimeOut
52085
wenzelm
parents: 52064
diff changeset
    35
      else (Exn.release test; Exn.release result)
41712
82339c3fd74a more robust TimeLimit: make double sure that watchdog has terminated and interrupts received during uninterruptible state are propagated (NB: Thread.testInterrupt requires InterruptSynch in Poly/ML 5.4.0 or earlier);
wenzelm
parents: 41710
diff changeset
    36
    end);
41710
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
    37
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
    38
end;
11ae688e4e30 clarified bootstrapping of structure TimeLimit;
wenzelm
parents:
diff changeset
    39