1 (* Title: HOL/Tools/Sledgehammer/async_manager.ML
2 Author: Fabian Immler, TU Muenchen
4 Author: Jasmin Blanchette, TU Muenchen
6 Central manager for asynchronous diagnosis tool threads.
9 signature ASYNC_MANAGER =
11 val break_into_chunks : string -> string list
13 string -> Time.time -> Time.time -> string * string
14 -> (unit -> bool * string) -> unit
15 val kill_threads : string -> string -> unit
16 val has_running_threads : string -> bool
17 val running_threads : string -> string -> unit
18 val thread_messages : string -> string -> int option -> unit
21 structure Async_Manager : ASYNC_MANAGER =
26 val message_store_limit = 20
27 val message_display_limit = 10
30 (** thread management **)
32 fun implode_message (workers, work) =
33 space_implode " " (Try.serial_commas "and" workers) ^ work
36 (* data structures over threads *)
38 structure Thread_Heap = Heap
40 type elem = Time.time * Thread.thread
41 fun ord ((a, _), (b, _)) = Time.compare (a, b)
44 fun lookup_thread xs = AList.lookup Thread.equal xs
45 fun delete_thread xs = AList.delete Thread.equal xs
46 fun update_thread xs = AList.update Thread.equal xs
49 (* state of thread manager *)
52 {manager: Thread.thread option,
53 timeout_heap: Thread_Heap.T,
56 * (string * Time.time * Time.time * (string * string))) list,
57 canceling: (Thread.thread * (string * Time.time * (string * string))) list,
58 messages: (bool * (string * (string * string))) list,
59 store: (string * (string * string)) list}
61 fun make_state manager timeout_heap active canceling messages store : state =
62 {manager = manager, timeout_heap = timeout_heap, active = active,
63 canceling = canceling, messages = messages, store = store}
65 val global_state = Synchronized.var "async_manager"
66 (make_state NONE Thread_Heap.empty [] [] [] [])
69 (* unregister thread *)
71 fun unregister (urgent, message) thread =
72 Synchronized.change global_state
73 (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
74 (case lookup_thread active thread of
75 SOME (tool, _, _, desc as (worker, its_desc)) =>
77 val active' = delete_thread thread active
79 val canceling' = (thread, (tool, now, desc)) :: canceling
81 (worker, its_desc ^ (if message = "" then "" else "\n" ^ message))
82 val messages' = (urgent, (tool, message')) :: messages
83 val store' = (tool, message') ::
84 (if length store <= message_store_limit then store
85 else #1 (chop message_store_limit store))
86 in make_state manager timeout_heap active' canceling' messages' store' end
90 (* main manager thread -- only one may exist *)
92 val min_wait_time = seconds 0.3
93 val max_wait_time = seconds 10.0
95 fun replace_all bef aft =
97 fun aux seen "" = String.implode (rev seen)
99 if String.isPrefix bef s then
100 aux seen "" ^ aft ^ aux [] (unprefix bef s)
102 aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
105 (* This is a workaround for Proof General's off-by-a-few sendback display bug,
106 whereby "pr" in "proof" is not highlighted. *)
107 val break_into_chunks = space_explode "\000" o replace_all "\n\n" "\000"
109 fun print_new_messages () =
110 Synchronized.change_result global_state
111 (fn {manager, timeout_heap, active, canceling, messages, store} =>
115 (null active andalso null canceling) orelse urgent)
116 ||> (fn postponed_messages =>
117 make_state manager timeout_heap active canceling
118 postponed_messages store))
119 |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker))
120 |> AList.group (op =)
121 |> List.app (fn ((_, ""), _) => ()
122 | ((tool, work), workers) =>
124 implode_message (workers |> sort_distinct string_ord, work)
126 |> List.app Output.urgent_message)
128 fun check_thread_manager () = Synchronized.change global_state
129 (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
130 if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
131 else let val manager = SOME (Toplevel.thread false (fn () =>
133 fun time_limit timeout_heap =
134 (case try Thread_Heap.min timeout_heap of
135 NONE => Time.+ (Time.now (), max_wait_time)
136 | SOME (time, _) => time)
138 (*action: find threads whose timeout is reached, and interrupt canceling threads*)
139 fun action {manager, timeout_heap, active, canceling, messages, store} =
140 let val (timeout_threads, timeout_heap') =
141 Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap
143 if null timeout_threads andalso null canceling then
147 val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling
148 val canceling' = filter (Thread.isActive o #1) canceling
149 val state' = make_state manager timeout_heap' active canceling' messages store
150 in SOME (map #2 timeout_threads, state') end
153 while Synchronized.change_result global_state
154 (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
155 if null active andalso null canceling andalso null messages
156 then (false, make_state NONE timeout_heap active canceling messages store)
159 (Synchronized.timed_access global_state
160 (SOME o time_limit o #timeout_heap) action
162 |> List.app (unregister (false, "Timed out."));
163 print_new_messages ();
164 (* give threads some time to respond to interrupt *)
165 OS.Process.sleep min_wait_time)
167 in make_state manager timeout_heap active canceling messages store end)
170 (* register thread *)
172 fun register tool birth_time death_time desc thread =
173 (Synchronized.change global_state
174 (fn {manager, timeout_heap, active, canceling, messages, store} =>
176 val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap
177 val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active
178 val state' = make_state manager timeout_heap' active' canceling messages store
180 check_thread_manager ())
183 fun launch tool birth_time death_time desc f =
184 (Toplevel.thread true
187 val self = Thread.self ()
188 val _ = register tool birth_time death_time desc self
189 in unregister (f ()) self end);
193 (** user commands **)
197 fun kill_threads tool das_wort_worker = Synchronized.change global_state
198 (fn {manager, timeout_heap, active, canceling, messages, store} =>
201 map_filter (fn (th, (tool', _, _, desc)) =>
202 if tool' = tool then SOME (th, (tool', Time.now (), desc))
204 val state' = make_state manager timeout_heap [] (killing @ canceling) messages store
206 if null killing then ()
207 else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.")
211 (* running threads *)
213 fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
215 fun has_running_threads tool =
216 exists (fn (_, (tool', _, _, _)) => tool' = tool)
217 (#active (Synchronized.value global_state))
219 fun running_threads tool das_wort_worker =
221 val {active, canceling, ...} = Synchronized.value global_state
222 val now = Time.now ()
223 fun running_info (_, (tool', birth_time, death_time, desc)) =
225 SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
226 seconds (Time.- (death_time, now)) ^ " to live:\n" ^
230 fun canceling_info (_, (tool', death_time, desc)) =
232 SOME ("Trying to interrupt " ^ das_wort_worker ^ " since " ^
233 seconds (Time.- (now, death_time)) ^ ":\n" ^ op ^ desc)
237 case map_filter running_info active of
238 [] => ["No " ^ das_wort_worker ^ "s running."]
239 | ss => "Running " ^ das_wort_worker ^ "s " :: ss
241 case map_filter canceling_info canceling of
243 | ss => "Interrupting " ^ das_wort_worker ^ "s " :: ss
244 in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
246 fun thread_messages tool das_wort_worker opt_limit =
248 val limit = the_default message_display_limit opt_limit
249 val tool_store = Synchronized.value global_state
250 |> #store |> filter (curry (op =) tool o fst)
252 "Recent " ^ das_wort_worker ^ " messages" ^
253 (if length tool_store <= limit then ":"
254 else " (" ^ string_of_int limit ^ " displayed):")
255 val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd)
256 in List.app Output.urgent_message (header :: maps break_into_chunks ss) end