author | wenzelm |
Sat, 02 Apr 2016 23:29:05 +0200 | |
changeset 62826 | eb94e570c1a4 |
parent 62519 | a564458f94db |
child 62923 | 3a122e1e352a |
permissions | -rw-r--r-- |
62519 | 1 |
(* Title: Pure/Concurrent/timeout.ML |
41710 | 2 |
Author: Makarius |
3 |
||
62519 | 4 |
Execution with (relative) timeout. |
41710 | 5 |
*) |
6 |
||
62519 | 7 |
signature TIMEOUT = |
41710 | 8 |
sig |
62519 | 9 |
exception TIMEOUT of Time.time |
10 |
val apply: Time.time -> ('a -> 'b) -> 'a -> 'b |
|
11 |
val print: Time.time -> string |
|
41710 | 12 |
end; |
13 |
||
62519 | 14 |
structure Timeout: TIMEOUT = |
41710 | 15 |
struct |
16 |
||
62519 | 17 |
exception TIMEOUT of Time.time; |
41710 | 18 |
|
62519 | 19 |
fun apply 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
|
20 |
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
|
21 |
let |
52051
9362fcd0318c
modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents:
44112
diff
changeset
|
22 |
val self = Thread.self (); |
62519 | 23 |
val start = Time.now (); |
52051
9362fcd0318c
modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents:
44112
diff
changeset
|
24 |
|
9362fcd0318c
modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents:
44112
diff
changeset
|
25 |
val request = |
62826 | 26 |
Event_Timer.request (start + timeout) |
61556 | 27 |
(fn () => Standard_Thread.interrupt_unsynchronized self); |
41714
3bafa8ba51db
always test/clear Multithreading.interrupted, indepently of thread attributes;
wenzelm
parents:
41712
diff
changeset
|
28 |
val result = |
3bafa8ba51db
always test/clear Multithreading.interrupted, indepently of thread attributes;
wenzelm
parents:
41712
diff
changeset
|
29 |
Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) (); |
41710 | 30 |
|
62519 | 31 |
val stop = Time.now (); |
52051
9362fcd0318c
modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents:
44112
diff
changeset
|
32 |
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
|
33 |
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
|
34 |
in |
52064
4b4ff1d3b723
back to more paranoid interrupt test after request is cancelled -- avoid race condition;
wenzelm
parents:
52051
diff
changeset
|
35 |
if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test) |
62826 | 36 |
then raise TIMEOUT (stop - start) |
52085 | 37 |
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
|
38 |
end); |
41710 | 39 |
|
62519 | 40 |
fun print t = "Timeout after " ^ Time.toString t ^ "s"; |
41 |
||
41710 | 42 |
end; |