author | hoelzl |
Wed, 02 Apr 2014 18:35:01 +0200 | |
changeset 56369 | 2704ca85be98 |
parent 52085 | 5534ec8b90a9 |
child 61182 | 9d0834562a78 |
permissions | -rw-r--r-- |
41710 | 1 |
(* Title: Pure/Concurrent/time_limit.ML |
2 |
Author: Makarius |
|
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 | 5 |
*) |
6 |
||
7 |
signature TIME_LIMIT = |
|
8 |
sig |
|
9 |
exception TimeOut |
|
10 |
val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b |
|
11 |
end; |
|
12 |
||
13 |
structure TimeLimit: TIME_LIMIT = |
|
14 |
struct |
|
15 |
||
16 |
exception TimeOut; |
|
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 | 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 | 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 | 37 |
|
38 |
end; |
|
39 |