1.1 --- a/src/HOL/Tools/ATP_Manager/async_manager.ML Wed Jul 28 11:42:48 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,241 +0,0 @@
1.4 -(* Title: HOL/Tools/ATP_Manager/async_manager.ML
1.5 - Author: Fabian Immler, TU Muenchen
1.6 - Author: Makarius
1.7 - Author: Jasmin Blanchette, TU Muenchen
1.8 -
1.9 -Central manager for asynchronous diagnosis tool threads.
1.10 -*)
1.11 -
1.12 -signature ASYNC_MANAGER =
1.13 -sig
1.14 - val launch :
1.15 - string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
1.16 - -> unit
1.17 - val kill_threads : string -> string -> unit
1.18 - val running_threads : string -> string -> unit
1.19 - val thread_messages : string -> string -> int option -> unit
1.20 -end;
1.21 -
1.22 -structure Async_Manager : ASYNC_MANAGER =
1.23 -struct
1.24 -
1.25 -(** preferences **)
1.26 -
1.27 -val message_store_limit = 20;
1.28 -val message_display_limit = 5;
1.29 -
1.30 -
1.31 -(** thread management **)
1.32 -
1.33 -(* data structures over threads *)
1.34 -
1.35 -structure Thread_Heap = Heap
1.36 -(
1.37 - type elem = Time.time * Thread.thread;
1.38 - fun ord ((a, _), (b, _)) = Time.compare (a, b);
1.39 -);
1.40 -
1.41 -fun lookup_thread xs = AList.lookup Thread.equal xs;
1.42 -fun delete_thread xs = AList.delete Thread.equal xs;
1.43 -fun update_thread xs = AList.update Thread.equal xs;
1.44 -
1.45 -
1.46 -(* state of thread manager *)
1.47 -
1.48 -type state =
1.49 - {manager: Thread.thread option,
1.50 - timeout_heap: Thread_Heap.T,
1.51 - active: (Thread.thread * (string * Time.time * Time.time * string)) list,
1.52 - canceling: (Thread.thread * (string * Time.time * string)) list,
1.53 - messages: (string * string) list,
1.54 - store: (string * string) list}
1.55 -
1.56 -fun make_state manager timeout_heap active canceling messages store : state =
1.57 - {manager = manager, timeout_heap = timeout_heap, active = active,
1.58 - canceling = canceling, messages = messages, store = store}
1.59 -
1.60 -val global_state = Synchronized.var "async_manager"
1.61 - (make_state NONE Thread_Heap.empty [] [] [] []);
1.62 -
1.63 -
1.64 -(* unregister thread *)
1.65 -
1.66 -fun unregister verbose message thread =
1.67 - Synchronized.change global_state
1.68 - (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
1.69 - (case lookup_thread active thread of
1.70 - SOME (tool, birth_time, _, desc) =>
1.71 - let
1.72 - val active' = delete_thread thread active;
1.73 - val now = Time.now ()
1.74 - val canceling' = (thread, (tool, now, desc)) :: canceling
1.75 - val message' =
1.76 - desc ^ "\n" ^ message ^
1.77 - (if verbose then
1.78 - "Total time: " ^ Int.toString (Time.toMilliseconds
1.79 - (Time.- (now, birth_time))) ^ " ms.\n"
1.80 - else
1.81 - "")
1.82 - val messages' = (tool, message') :: messages;
1.83 - val store' = (tool, message') ::
1.84 - (if length store <= message_store_limit then store
1.85 - else #1 (chop message_store_limit store));
1.86 - in make_state manager timeout_heap active' canceling' messages' store' end
1.87 - | NONE => state));
1.88 -
1.89 -
1.90 -(* main manager thread -- only one may exist *)
1.91 -
1.92 -val min_wait_time = Time.fromMilliseconds 300;
1.93 -val max_wait_time = Time.fromSeconds 10;
1.94 -
1.95 -fun replace_all bef aft =
1.96 - let
1.97 - fun aux seen "" = String.implode (rev seen)
1.98 - | aux seen s =
1.99 - if String.isPrefix bef s then
1.100 - aux seen "" ^ aft ^ aux [] (unprefix bef s)
1.101 - else
1.102 - aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
1.103 - in aux [] end
1.104 -
1.105 -(* This is a workaround for Proof General's off-by-a-few sendback display bug,
1.106 - whereby "pr" in "proof" is not highlighted. *)
1.107 -fun break_into_chunks xs =
1.108 - maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) xs
1.109 -
1.110 -fun print_new_messages () =
1.111 - case Synchronized.change_result global_state
1.112 - (fn {manager, timeout_heap, active, canceling, messages, store} =>
1.113 - (messages, make_state manager timeout_heap active canceling []
1.114 - store)) of
1.115 - [] => ()
1.116 - | msgs as (tool, _) :: _ =>
1.117 - let val ss = break_into_chunks msgs in
1.118 - List.app priority (tool ^ ": " ^ hd ss :: tl ss)
1.119 - end
1.120 -
1.121 -fun check_thread_manager verbose = Synchronized.change global_state
1.122 - (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
1.123 - if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
1.124 - else let val manager = SOME (Toplevel.thread false (fn () =>
1.125 - let
1.126 - fun time_limit timeout_heap =
1.127 - (case try Thread_Heap.min timeout_heap of
1.128 - NONE => Time.+ (Time.now (), max_wait_time)
1.129 - | SOME (time, _) => time);
1.130 -
1.131 - (*action: find threads whose timeout is reached, and interrupt canceling threads*)
1.132 - fun action {manager, timeout_heap, active, canceling, messages, store} =
1.133 - let val (timeout_threads, timeout_heap') =
1.134 - Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
1.135 - in
1.136 - if null timeout_threads andalso null canceling then
1.137 - NONE
1.138 - else
1.139 - let
1.140 - val _ = List.app (Simple_Thread.interrupt o #1) canceling
1.141 - val canceling' = filter (Thread.isActive o #1) canceling
1.142 - val state' = make_state manager timeout_heap' active canceling' messages store;
1.143 - in SOME (map #2 timeout_threads, state') end
1.144 - end;
1.145 - in
1.146 - while Synchronized.change_result global_state
1.147 - (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
1.148 - if null active andalso null canceling andalso null messages
1.149 - then (false, make_state NONE timeout_heap active canceling messages store)
1.150 - else (true, state))
1.151 - do
1.152 - (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
1.153 - |> these
1.154 - |> List.app (unregister verbose "Timed out.\n");
1.155 - print_new_messages ();
1.156 - (*give threads some time to respond to interrupt*)
1.157 - OS.Process.sleep min_wait_time)
1.158 - end))
1.159 - in make_state manager timeout_heap active canceling messages store end)
1.160 -
1.161 -
1.162 -(* register thread *)
1.163 -
1.164 -fun register tool verbose birth_time death_time desc thread =
1.165 - (Synchronized.change global_state
1.166 - (fn {manager, timeout_heap, active, canceling, messages, store} =>
1.167 - let
1.168 - val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
1.169 - val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
1.170 - val state' = make_state manager timeout_heap' active' canceling messages store;
1.171 - in state' end);
1.172 - check_thread_manager verbose);
1.173 -
1.174 -
1.175 -fun launch tool verbose birth_time death_time desc f =
1.176 - (Toplevel.thread true
1.177 - (fn () =>
1.178 - let
1.179 - val self = Thread.self ()
1.180 - val _ = register tool verbose birth_time death_time desc self
1.181 - val message = f ()
1.182 - in unregister verbose message self end);
1.183 - ())
1.184 -
1.185 -
1.186 -(** user commands **)
1.187 -
1.188 -(* kill threads *)
1.189 -
1.190 -fun kill_threads tool workers = Synchronized.change global_state
1.191 - (fn {manager, timeout_heap, active, canceling, messages, store} =>
1.192 - let
1.193 - val killing =
1.194 - map_filter (fn (th, (tool', _, _, desc)) =>
1.195 - if tool' = tool then SOME (th, (tool', Time.now (), desc))
1.196 - else NONE) active
1.197 - val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
1.198 - val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
1.199 - in state' end);
1.200 -
1.201 -
1.202 -(* running threads *)
1.203 -
1.204 -fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
1.205 -
1.206 -fun running_threads tool workers =
1.207 - let
1.208 - val {active, canceling, ...} = Synchronized.value global_state;
1.209 -
1.210 - val now = Time.now ();
1.211 - fun running_info (_, (tool', birth_time, death_time, desc)) =
1.212 - if tool' = tool then
1.213 - SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
1.214 - seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
1.215 - else
1.216 - NONE
1.217 - fun canceling_info (_, (tool', death_time, desc)) =
1.218 - if tool' = tool then
1.219 - SOME ("Trying to interrupt thread since " ^
1.220 - seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
1.221 - else
1.222 - NONE
1.223 - val running =
1.224 - case map_filter running_info active of
1.225 - [] => ["No " ^ workers ^ " running."]
1.226 - | ss => "Running " ^ workers ^ ":" :: ss
1.227 - val interrupting =
1.228 - case map_filter canceling_info canceling of
1.229 - [] => []
1.230 - | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
1.231 - in priority (space_implode "\n\n" (running @ interrupting)) end
1.232 -
1.233 -fun thread_messages tool worker opt_limit =
1.234 - let
1.235 - val limit = the_default message_display_limit opt_limit;
1.236 - val tool_store = Synchronized.value global_state
1.237 - |> #store |> filter (curry (op =) tool o fst)
1.238 - val header =
1.239 - "Recent " ^ worker ^ " messages" ^
1.240 - (if length tool_store <= limit then ":"
1.241 - else " (" ^ string_of_int limit ^ " displayed):");
1.242 - in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end
1.243 -
1.244 -end;