author | wenzelm |
Mon, 25 Mar 2019 14:40:28 +0100 | |
changeset 69975 | 35cc58a54ffc |
parent 69826 | 1bea05713dde |
child 71692 | f8e52c0152fe |
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 = |
62923 | 20 |
Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts => |
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
|
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 = |
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
67000
diff
changeset
|
26 |
Event_Timer.request {physical = false} (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 = |
62923 | 29 |
Exn.capture (fn () => Thread_Attributes.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); |
62924
ce47945ce4fb
tuned signature -- closer to Exn.Interrupt.expose in Scala;
wenzelm
parents:
62923
diff
changeset
|
33 |
val test = Exn.capture Thread_Attributes.expose_interrupt (); |
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 |
|
67000
1698e9ccef2d
more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
wenzelm
parents:
62924
diff
changeset
|
40 |
fun print t = "Timeout after " ^ Value.print_time t ^ "s"; |
62519 | 41 |
|
41710 | 42 |
end; |