|
1 (* Title: HOL/Tools/Sledgehammer/async_manager_legacy.ML |
|
2 Author: Fabian Immler, TU Muenchen |
|
3 Author: Makarius |
|
4 Author: Jasmin Blanchette, TU Muenchen |
|
5 |
|
6 Central manager for asynchronous diagnosis tool threads. |
|
7 |
|
8 Proof General legacy! |
|
9 *) |
|
10 |
|
11 signature ASYNC_MANAGER_LEGACY = |
|
12 sig |
|
13 val break_into_chunks : string -> string list |
|
14 val thread : string -> Time.time -> Time.time -> string * string -> (unit -> bool * string) -> |
|
15 unit |
|
16 val kill_threads : string -> string -> unit |
|
17 val has_running_threads : string -> bool |
|
18 val running_threads : string -> string -> unit |
|
19 val thread_messages : string -> string -> int option -> unit |
|
20 end; |
|
21 |
|
22 structure Async_Manager_Legacy : ASYNC_MANAGER_LEGACY = |
|
23 struct |
|
24 |
|
25 fun make_thread interrupts body = |
|
26 Thread.fork |
|
27 (fn () => |
|
28 Runtime.debugging NONE body () handle exn => |
|
29 if Exn.is_interrupt exn then () |
|
30 else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn), |
|
31 Simple_Thread.attributes {stack_limit = NONE, interrupts = interrupts}); |
|
32 |
|
33 val message_store_limit = 20 |
|
34 val message_display_limit = 10 |
|
35 |
|
36 fun implode_message (workers, work) = |
|
37 space_implode " " (Try.serial_commas "and" workers) ^ work |
|
38 |
|
39 structure Thread_Heap = Heap |
|
40 ( |
|
41 type elem = Time.time * Thread.thread |
|
42 fun ord ((a, _), (b, _)) = Time.compare (a, b) |
|
43 ) |
|
44 |
|
45 fun lookup_thread xs = AList.lookup Thread.equal xs |
|
46 fun delete_thread xs = AList.delete Thread.equal xs |
|
47 fun update_thread xs = AList.update Thread.equal xs |
|
48 |
|
49 type state = |
|
50 {manager: Thread.thread option, |
|
51 timeout_heap: Thread_Heap.T, |
|
52 active: |
|
53 (Thread.thread |
|
54 * (string * Time.time * Time.time * (string * string))) list, |
|
55 canceling: (Thread.thread * (string * Time.time * (string * string))) list, |
|
56 messages: (bool * (string * (string * string))) list, |
|
57 store: (string * (string * string)) list} |
|
58 |
|
59 fun make_state manager timeout_heap active canceling messages store : state = |
|
60 {manager = manager, timeout_heap = timeout_heap, active = active, |
|
61 canceling = canceling, messages = messages, store = store} |
|
62 |
|
63 val global_state = Synchronized.var "async_manager" (make_state NONE Thread_Heap.empty [] [] [] []) |
|
64 |
|
65 fun unregister (urgent, message) thread = |
|
66 Synchronized.change global_state |
|
67 (fn state as {manager, timeout_heap, active, canceling, messages, store} => |
|
68 (case lookup_thread active thread of |
|
69 SOME (tool, _, _, desc as (worker, its_desc)) => |
|
70 let |
|
71 val active' = delete_thread thread active |
|
72 val now = Time.now () |
|
73 val canceling' = (thread, (tool, now, desc)) :: canceling |
|
74 val message' = |
|
75 (worker, its_desc ^ (if message = "" then "" else "\n" ^ message)) |
|
76 val messages' = (urgent, (tool, message')) :: messages |
|
77 val store' = (tool, message') :: |
|
78 (if length store <= message_store_limit then store |
|
79 else #1 (chop message_store_limit store)) |
|
80 in make_state manager timeout_heap active' canceling' messages' store' end |
|
81 | NONE => state)) |
|
82 |
|
83 val min_wait_time = seconds 0.3 |
|
84 val max_wait_time = seconds 10.0 |
|
85 |
|
86 fun replace_all bef aft = |
|
87 let |
|
88 fun aux seen "" = String.implode (rev seen) |
|
89 | aux seen s = |
|
90 if String.isPrefix bef s then |
|
91 aux seen "" ^ aft ^ aux [] (unprefix bef s) |
|
92 else |
|
93 aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) |
|
94 in aux [] end |
|
95 |
|
96 (* This is a workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in |
|
97 "proof" is not highlighted. *) |
|
98 val break_into_chunks = space_explode "\000" o replace_all "\n\n" "\000" |
|
99 |
|
100 fun print_new_messages () = |
|
101 Synchronized.change_result global_state |
|
102 (fn {manager, timeout_heap, active, canceling, messages, store} => |
|
103 messages |
|
104 |> List.partition |
|
105 (fn (urgent, _) => |
|
106 (null active andalso null canceling) orelse urgent) |
|
107 ||> (fn postponed_messages => |
|
108 make_state manager timeout_heap active canceling |
|
109 postponed_messages store)) |
|
110 |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker)) |
|
111 |> AList.group (op =) |
|
112 |> List.app (fn ((_, ""), _) => () |
|
113 | ((tool, work), workers) => |
|
114 tool ^ ": " ^ |
|
115 implode_message (workers |> sort_distinct string_ord, work) |
|
116 |> break_into_chunks |
|
117 |> List.app writeln) |
|
118 |
|
119 fun check_thread_manager () = Synchronized.change global_state |
|
120 (fn state as {manager, timeout_heap, active, canceling, messages, store} => |
|
121 if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state |
|
122 else let val manager = SOME (make_thread false (fn () => |
|
123 let |
|
124 fun time_limit timeout_heap = |
|
125 (case try Thread_Heap.min timeout_heap of |
|
126 NONE => Time.+ (Time.now (), max_wait_time) |
|
127 | SOME (time, _) => time) |
|
128 |
|
129 (*action: find threads whose timeout is reached, and interrupt canceling threads*) |
|
130 fun action {manager, timeout_heap, active, canceling, messages, store} = |
|
131 let val (timeout_threads, timeout_heap') = |
|
132 Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap |
|
133 in |
|
134 if null timeout_threads andalso null canceling then |
|
135 NONE |
|
136 else |
|
137 let |
|
138 val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling |
|
139 val canceling' = filter (Thread.isActive o #1) canceling |
|
140 val state' = make_state manager timeout_heap' active canceling' messages store |
|
141 in SOME (map #2 timeout_threads, state') end |
|
142 end |
|
143 in |
|
144 while Synchronized.change_result global_state |
|
145 (fn state as {timeout_heap, active, canceling, messages, store, ...} => |
|
146 if null active andalso null canceling andalso null messages |
|
147 then (false, make_state NONE timeout_heap active canceling messages store) |
|
148 else (true, state)) |
|
149 do |
|
150 (Synchronized.timed_access global_state |
|
151 (SOME o time_limit o #timeout_heap) action |
|
152 |> these |
|
153 |> List.app (unregister (false, "Timed out.")); |
|
154 print_new_messages (); |
|
155 (* give threads some time to respond to interrupt *) |
|
156 OS.Process.sleep min_wait_time) |
|
157 end)) |
|
158 in make_state manager timeout_heap active canceling messages store end) |
|
159 |
|
160 fun register tool birth_time death_time desc thread = |
|
161 (Synchronized.change global_state |
|
162 (fn {manager, timeout_heap, active, canceling, messages, store} => |
|
163 let |
|
164 val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap |
|
165 val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active |
|
166 val state' = make_state manager timeout_heap' active' canceling messages store |
|
167 in state' end); |
|
168 check_thread_manager ()) |
|
169 |
|
170 fun thread tool birth_time death_time desc f = |
|
171 (make_thread true |
|
172 (fn () => |
|
173 let |
|
174 val self = Thread.self () |
|
175 val _ = register tool birth_time death_time desc self |
|
176 in unregister (f ()) self end); |
|
177 ()) |
|
178 |
|
179 fun kill_threads tool das_wort_worker = Synchronized.change global_state |
|
180 (fn {manager, timeout_heap, active, canceling, messages, store} => |
|
181 let |
|
182 val killing = |
|
183 map_filter (fn (th, (tool', _, _, desc)) => |
|
184 if tool' = tool then SOME (th, (tool', Time.now (), desc)) |
|
185 else NONE) active |
|
186 val state' = make_state manager timeout_heap [] (killing @ canceling) messages store |
|
187 val _ = |
|
188 if null killing then () |
|
189 else writeln ("Interrupted active " ^ das_wort_worker ^ "s.") |
|
190 in state' end) |
|
191 |
|
192 fun str_of_time time = string_of_int (Time.toSeconds time) ^ " s" |
|
193 |
|
194 fun has_running_threads tool = |
|
195 exists (fn (_, (tool', _, _, _)) => tool' = tool) (#active (Synchronized.value global_state)) |
|
196 |
|
197 fun running_threads tool das_wort_worker = |
|
198 let |
|
199 val {active, canceling, ...} = Synchronized.value global_state |
|
200 val now = Time.now () |
|
201 fun running_info (_, (tool', birth_time, death_time, desc)) = |
|
202 if tool' = tool then |
|
203 SOME ("Running: " ^ str_of_time (Time.- (now, birth_time)) ^ " -- " ^ |
|
204 str_of_time (Time.- (death_time, now)) ^ " to live:\n" ^ op ^ desc) |
|
205 else |
|
206 NONE |
|
207 fun canceling_info (_, (tool', death_time, desc)) = |
|
208 if tool' = tool then |
|
209 SOME ("Trying to interrupt " ^ das_wort_worker ^ " since " ^ |
|
210 str_of_time (Time.- (now, death_time)) ^ ":\n" ^ op ^ desc) |
|
211 else |
|
212 NONE |
|
213 val running = |
|
214 case map_filter running_info active of |
|
215 [] => ["No " ^ das_wort_worker ^ "s running."] |
|
216 | ss => "Running " ^ das_wort_worker ^ "s" :: ss |
|
217 val interrupting = |
|
218 case map_filter canceling_info canceling of |
|
219 [] => [] |
|
220 | ss => "Interrupting " ^ das_wort_worker ^ "s" :: ss |
|
221 in writeln (space_implode "\n\n" (running @ interrupting)) end |
|
222 |
|
223 fun thread_messages tool das_wort_worker opt_limit = |
|
224 let |
|
225 val limit = the_default message_display_limit opt_limit |
|
226 val tool_store = Synchronized.value global_state |
|
227 |> #store |> filter (curry (op =) tool o fst) |
|
228 val header = |
|
229 "Recent " ^ das_wort_worker ^ " messages" ^ |
|
230 (if length tool_store <= limit then ":" |
|
231 else " (" ^ string_of_int limit ^ " displayed):") |
|
232 val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd) |
|
233 in List.app writeln (header :: maps break_into_chunks ss) end |
|
234 |
|
235 end; |