author | wenzelm |
Fri, 05 Mar 2021 17:29:49 +0100 | |
changeset 73387 | 3b5196dac4c8 |
parent 71692 | f8e52c0152fe |
child 73388 | a40e69fde2b4 |
permissions | -rw-r--r-- |
62519 | 1 |
(* Title: Pure/Concurrent/timeout.ML |
41710 | 2 |
Author: Makarius |
3 |
||
73387 | 4 |
Execution with relative timeout: |
5 |
- timeout specification < 1ms means no timeout |
|
6 |
- actual timeout is subject to system option "timeout_scale" |
|
41710 | 7 |
*) |
8 |
||
62519 | 9 |
signature TIMEOUT = |
41710 | 10 |
sig |
62519 | 11 |
exception TIMEOUT of Time.time |
73387 | 12 |
val scale: unit -> real |
13 |
val scale_time: Time.time -> Time.time |
|
14 |
val end_time: Time.time -> Time.time |
|
62519 | 15 |
val apply: Time.time -> ('a -> 'b) -> 'a -> 'b |
16 |
val print: Time.time -> string |
|
41710 | 17 |
end; |
18 |
||
62519 | 19 |
structure Timeout: TIMEOUT = |
41710 | 20 |
struct |
21 |
||
62519 | 22 |
exception TIMEOUT of Time.time; |
41710 | 23 |
|
73387 | 24 |
fun scale () = Options.default_real "timeout_scale"; |
25 |
fun scale_time t = Time.scale (scale ()) t; |
|
26 |
||
27 |
fun end_time timeout = Time.now () + scale_time timeout; |
|
28 |
||
62519 | 29 |
fun apply timeout f x = |
73387 | 30 |
if timeout < Time.fromMilliseconds 1 then f x |
31 |
else |
|
32 |
Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts => |
|
33 |
let |
|
34 |
val self = Thread.self (); |
|
35 |
val start = Time.now (); |
|
52051
9362fcd0318c
modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
wenzelm
parents:
44112
diff
changeset
|
36 |
|
73387 | 37 |
val request = |
38 |
Event_Timer.request {physical = false} (start + scale_time timeout) |
|
39 |
(fn () => Isabelle_Thread.interrupt_unsynchronized self); |
|
40 |
val result = |
|
41 |
Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) (); |
|
41710 | 42 |
|
73387 | 43 |
val stop = Time.now (); |
44 |
val was_timeout = not (Event_Timer.cancel request); |
|
45 |
val test = Exn.capture Thread_Attributes.expose_interrupt (); |
|
46 |
in |
|
47 |
if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test) |
|
48 |
then raise TIMEOUT (stop - start) |
|
49 |
else (Exn.release test; Exn.release result) |
|
50 |
end); |
|
41710 | 51 |
|
67000
1698e9ccef2d
more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
wenzelm
parents:
62924
diff
changeset
|
52 |
fun print t = "Timeout after " ^ Value.print_time t ^ "s"; |
62519 | 53 |
|
41710 | 54 |
end; |