author | wenzelm |
Tue, 26 Sep 2023 12:46:31 +0200 | |
changeset 78716 | 97dfba4405e3 |
parent 78648 | 852ec09aef13 |
child 78720 | 909dc00766a0 |
permissions | -rw-r--r-- |
52050 | 1 |
(* Title: Pure/Concurrent/event_timer.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Initiate event after given point in time. |
|
5 |
||
6 |
Note: events are run as synchronized action within a dedicated thread |
|
7 |
and should finish quickly without further ado. |
|
8 |
*) |
|
9 |
||
10 |
signature EVENT_TIMER = |
|
11 |
sig |
|
69824 | 12 |
type request |
13 |
val eq_request: request * request -> bool |
|
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
14 |
val request: {physical: bool} -> Time.time -> (unit -> unit) -> request |
52050 | 15 |
val cancel: request -> bool |
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
16 |
val future: {physical: bool} -> Time.time -> unit future |
52050 | 17 |
val shutdown: unit -> unit |
18 |
end; |
|
19 |
||
20 |
structure Event_Timer: EVENT_TIMER = |
|
21 |
struct |
|
22 |
||
23 |
(* type request *) |
|
24 |
||
69825 | 25 |
datatype request = |
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
26 |
Request of {id: int, gc_start: Time.time option, time: Time.time, event: unit -> unit}; |
69825 | 27 |
|
28 |
val new_id = Counter.make (); |
|
69824 | 29 |
|
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
30 |
fun new_request physical time event = |
69825 | 31 |
Request { |
32 |
id = new_id (), |
|
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
33 |
gc_start = if physical then NONE else SOME (ML_Heap.gc_now ()), |
69825 | 34 |
time = time, |
35 |
event = event}; |
|
69824 | 36 |
|
37 |
fun eq_request (Request {id = id1, ...}, Request {id = id2, ...}) = id1 = id2; |
|
52050 | 38 |
|
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
39 |
fun request_gc_start (Request {gc_start, ...}) = gc_start; |
69825 | 40 |
fun request_time (Request {time, ...}) = time; |
41 |
fun request_event (Request {event, ...}) = event; |
|
42 |
||
52050 | 43 |
|
44 |
(* type requests *) |
|
45 |
||
46 |
structure Requests = Table(type key = Time.time val ord = Time.compare); |
|
69824 | 47 |
type requests = request list Requests.table; |
52050 | 48 |
|
69824 | 49 |
fun add req_time req (requests: requests) = |
50 |
Requests.cons_list (req_time, req) requests; |
|
52050 | 51 |
|
69824 | 52 |
fun del req (requests: requests) = |
52050 | 53 |
let |
69824 | 54 |
val old = |
55 |
requests |> Requests.get_first (fn (key, reqs) => |
|
56 |
reqs |> get_first (fn req' => |
|
57 |
if eq_request (req', req) then SOME (key, req') else NONE)); |
|
52050 | 58 |
in |
69824 | 59 |
(case old of |
52050 | 60 |
NONE => (false, requests) |
69824 | 61 |
| SOME req' => (true, Requests.remove_list eq_request req' requests)) |
52050 | 62 |
end; |
63 |
||
69824 | 64 |
fun next_time (requests: requests) = |
65 |
Option.map #1 (Requests.min requests); |
|
52050 | 66 |
|
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
67 |
fun next_event (now, gc_now) (requests: requests) = |
52050 | 68 |
(case Requests.min requests of |
69 |
NONE => NONE |
|
69824 | 70 |
| SOME (req_time, reqs) => |
69825 | 71 |
if now < req_time then NONE |
52050 | 72 |
else |
73 |
let |
|
69825 | 74 |
val (reqs', req) = split_last reqs; |
52050 | 75 |
val requests' = |
69824 | 76 |
if null reqs' |
77 |
then Requests.delete req_time requests |
|
78 |
else Requests.update (req_time, reqs') requests; |
|
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
79 |
val req_time' = |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
80 |
(case request_gc_start req of |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
81 |
NONE => req_time |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
82 |
| SOME gc_start => request_time req + (gc_now - gc_start)); |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
83 |
in |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
84 |
if now < req_time' |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
85 |
then (fn () => (), add req_time' req requests') |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
86 |
else (request_event req, requests') |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
87 |
end |> SOME); |
52050 | 88 |
|
89 |
||
90 |
(* global state *) |
|
91 |
||
59329
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
92 |
datatype status = Normal | Shutdown_Req | Shutdown_Ack; |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
93 |
|
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
94 |
datatype state = |
78648 | 95 |
State of {requests: requests, status: status, manager: Isabelle_Thread.T option}; |
59329
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
96 |
|
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
97 |
fun make_state (requests, status, manager) = |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
98 |
State {requests = requests, status = status, manager = manager}; |
52050 | 99 |
|
59329
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
100 |
val normal_state = make_state (Requests.empty, Normal, NONE); |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
101 |
val shutdown_ack_state = make_state (Requests.empty, Shutdown_Ack, NONE); |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
102 |
|
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
103 |
fun is_shutdown s (State {requests, status, manager}) = |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
104 |
Requests.is_empty requests andalso status = s andalso is_none manager; |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
105 |
|
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
106 |
fun is_shutdown_req (State {requests, status, ...}) = |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
107 |
Requests.is_empty requests andalso status = Shutdown_Req; |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
108 |
|
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
109 |
val state = Synchronized.var "Event_Timer.state" normal_state; |
52050 | 110 |
|
111 |
||
112 |
(* manager thread *) |
|
113 |
||
114 |
fun manager_loop () = |
|
59329
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
115 |
if Synchronized.timed_access state |
69824 | 116 |
(fn State {requests, ...} => next_time requests) |
59329
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
117 |
(fn st as State {requests, status, manager} => |
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
118 |
(case next_event (Time.now (), ML_Heap.gc_now ()) requests of |
59329
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
119 |
SOME (event, requests') => |
59337 | 120 |
let |
121 |
val _ = Exn.capture event (); |
|
122 |
val state' = make_state (requests', status, manager); |
|
123 |
in SOME (true, state') end |
|
59329
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
124 |
| NONE => |
59337 | 125 |
if is_shutdown_req st |
126 |
then SOME (false, shutdown_ack_state) |
|
59339 | 127 |
else NONE)) <> SOME false |
128 |
then manager_loop () else (); |
|
52050 | 129 |
|
130 |
fun manager_check manager = |
|
78648 | 131 |
if is_some manager andalso Isabelle_Thread.is_active (the manager) then manager |
60764 | 132 |
else |
71692 | 133 |
SOME (Isabelle_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false} |
60764 | 134 |
manager_loop); |
52050 | 135 |
|
136 |
fun shutdown () = |
|
78716 | 137 |
Thread_Attributes.uninterruptible (fn run => fn () => |
62239 | 138 |
if Synchronized.change_result state (fn st as State {requests, manager, ...} => |
59337 | 139 |
if is_shutdown Normal st then (false, st) |
140 |
else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then |
|
59329
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
141 |
raise Fail "Concurrent attempt to shutdown event timer" |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
142 |
else (true, make_state (requests, Shutdown_Req, manager_check manager))) |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
143 |
then |
78716 | 144 |
run (fn () => |
59329
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
145 |
Synchronized.guarded_access state |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
146 |
(fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE)) () |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
147 |
handle exn => |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
148 |
if Exn.is_interrupt exn then |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
149 |
Synchronized.change state (fn State {requests, manager, ...} => |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
150 |
make_state (requests, Normal, manager)) |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
151 |
else () |
72278d083d3a
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
wenzelm
parents:
56768
diff
changeset
|
152 |
else ()) (); |
52050 | 153 |
|
52798
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52589
diff
changeset
|
154 |
|
59339 | 155 |
(* main operations *) |
156 |
||
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
157 |
fun request {physical} time event = |
59339 | 158 |
Synchronized.change_result state (fn State {requests, status, manager} => |
159 |
let |
|
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
160 |
val req = new_request physical time event; |
69824 | 161 |
val requests' = add time req requests; |
59339 | 162 |
val manager' = manager_check manager; |
163 |
in (req, make_state (requests', status, manager')) end); |
|
164 |
||
165 |
fun cancel req = |
|
166 |
Synchronized.change_result state (fn State {requests, status, manager} => |
|
167 |
let |
|
69824 | 168 |
val (canceled, requests') = del req requests; |
59339 | 169 |
val manager' = manager_check manager; |
170 |
in (canceled, make_state (requests', status, manager')) end); |
|
52798
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52589
diff
changeset
|
171 |
|
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
172 |
fun future physical time = |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
173 |
Thread_Attributes.uninterruptible (fn _ => fn () => |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
174 |
let |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
175 |
val req: request Single_Assignment.var = Single_Assignment.var "req"; |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
176 |
fun abort () = ignore (cancel (Single_Assignment.await req)); |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
177 |
val promise: unit future = Future.promise_name "event_timer" abort; |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
178 |
val _ = Single_Assignment.assign req (request physical time (Future.fulfill promise)); |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
69825
diff
changeset
|
179 |
in promise end) (); |
52798
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52589
diff
changeset
|
180 |
|
52050 | 181 |
end; |