diff -r 483879af0643 -r e34b099e477e src/HOL/Tools/ATP/async_manager.ML --- a/src/HOL/Tools/ATP/async_manager.ML Tue Aug 31 23:50:59 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,241 +0,0 @@ -(* Title: HOL/Tools/ATP/async_manager.ML - Author: Fabian Immler, TU Muenchen - Author: Makarius - Author: Jasmin Blanchette, TU Muenchen - -Central manager for asynchronous diagnosis tool threads. -*) - -signature ASYNC_MANAGER = -sig - val launch : - string -> bool -> Time.time -> Time.time -> string -> (unit -> string) - -> unit - val kill_threads : string -> string -> unit - val running_threads : string -> string -> unit - val thread_messages : string -> string -> int option -> unit -end; - -structure Async_Manager : ASYNC_MANAGER = -struct - -(** preferences **) - -val message_store_limit = 20; -val message_display_limit = 5; - - -(** thread management **) - -(* data structures over threads *) - -structure Thread_Heap = Heap -( - type elem = Time.time * Thread.thread; - fun ord ((a, _), (b, _)) = Time.compare (a, b); -); - -fun lookup_thread xs = AList.lookup Thread.equal xs; -fun delete_thread xs = AList.delete Thread.equal xs; -fun update_thread xs = AList.update Thread.equal xs; - - -(* state of thread manager *) - -type state = - {manager: Thread.thread option, - timeout_heap: Thread_Heap.T, - active: (Thread.thread * (string * Time.time * Time.time * string)) list, - canceling: (Thread.thread * (string * Time.time * string)) list, - messages: (string * string) list, - store: (string * string) list} - -fun make_state manager timeout_heap active canceling messages store : state = - {manager = manager, timeout_heap = timeout_heap, active = active, - canceling = canceling, messages = messages, store = store} - -val global_state = Synchronized.var "async_manager" - (make_state NONE Thread_Heap.empty [] [] [] []); - - -(* unregister thread *) - -fun unregister verbose message thread = - Synchronized.change global_state - (fn state as {manager, timeout_heap, active, canceling, messages, store} => - (case lookup_thread active thread of - SOME (tool, birth_time, _, desc) => - let - val active' = delete_thread thread active; - val now = Time.now () - val canceling' = (thread, (tool, now, desc)) :: canceling - val message' = - desc ^ "\n" ^ message ^ - (if verbose then - "\nTotal time: " ^ Int.toString (Time.toMilliseconds - (Time.- (now, birth_time))) ^ " ms." - else - "") - val messages' = (tool, message') :: messages; - val store' = (tool, message') :: - (if length store <= message_store_limit then store - else #1 (chop message_store_limit store)); - in make_state manager timeout_heap active' canceling' messages' store' end - | NONE => state)); - - -(* main manager thread -- only one may exist *) - -val min_wait_time = Time.fromMilliseconds 300; -val max_wait_time = Time.fromSeconds 10; - -fun replace_all bef aft = - let - fun aux seen "" = String.implode (rev seen) - | aux seen s = - if String.isPrefix bef s then - aux seen "" ^ aft ^ aux [] (unprefix bef s) - else - aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) - in aux [] end - -(* This is a workaround for Proof General's off-by-a-few sendback display bug, - whereby "pr" in "proof" is not highlighted. *) -fun break_into_chunks xs = - maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) xs - -fun print_new_messages () = - case Synchronized.change_result global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - (messages, make_state manager timeout_heap active canceling [] - store)) of - [] => () - | msgs as (tool, _) :: _ => - let val ss = break_into_chunks msgs in - List.app priority (tool ^ ": " ^ hd ss :: tl ss) - end - -fun check_thread_manager verbose = Synchronized.change global_state - (fn state as {manager, timeout_heap, active, canceling, messages, store} => - if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state - else let val manager = SOME (Toplevel.thread false (fn () => - let - fun time_limit timeout_heap = - (case try Thread_Heap.min timeout_heap of - NONE => Time.+ (Time.now (), max_wait_time) - | SOME (time, _) => time); - - (*action: find threads whose timeout is reached, and interrupt canceling threads*) - fun action {manager, timeout_heap, active, canceling, messages, store} = - let val (timeout_threads, timeout_heap') = - Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap; - in - if null timeout_threads andalso null canceling then - NONE - else - let - val _ = List.app (Simple_Thread.interrupt o #1) canceling - val canceling' = filter (Thread.isActive o #1) canceling - val state' = make_state manager timeout_heap' active canceling' messages store; - in SOME (map #2 timeout_threads, state') end - end; - in - while Synchronized.change_result global_state - (fn state as {timeout_heap, active, canceling, messages, store, ...} => - if null active andalso null canceling andalso null messages - then (false, make_state NONE timeout_heap active canceling messages store) - else (true, state)) - do - (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action - |> these - |> List.app (unregister verbose "Timed out.\n"); - print_new_messages (); - (*give threads some time to respond to interrupt*) - OS.Process.sleep min_wait_time) - end)) - in make_state manager timeout_heap active canceling messages store end) - - -(* register thread *) - -fun register tool verbose birth_time death_time desc thread = - (Synchronized.change global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - let - val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap; - val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active; - val state' = make_state manager timeout_heap' active' canceling messages store; - in state' end); - check_thread_manager verbose); - - -fun launch tool verbose birth_time death_time desc f = - (Toplevel.thread true - (fn () => - let - val self = Thread.self () - val _ = register tool verbose birth_time death_time desc self - val message = f () - in unregister verbose message self end); - ()) - - -(** user commands **) - -(* kill threads *) - -fun kill_threads tool workers = Synchronized.change global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - let - val killing = - map_filter (fn (th, (tool', _, _, desc)) => - if tool' = tool then SOME (th, (tool', Time.now (), desc)) - else NONE) active - val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; - val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".") - in state' end); - - -(* running threads *) - -fun seconds time = string_of_int (Time.toSeconds time) ^ " s" - -fun running_threads tool workers = - let - val {active, canceling, ...} = Synchronized.value global_state; - - val now = Time.now (); - fun running_info (_, (tool', birth_time, death_time, desc)) = - if tool' = tool then - SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^ - seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc) - else - NONE - fun canceling_info (_, (tool', death_time, desc)) = - if tool' = tool then - SOME ("Trying to interrupt thread since " ^ - seconds (Time.- (now, death_time)) ^ ":\n" ^ desc) - else - NONE - val running = - case map_filter running_info active of - [] => ["No " ^ workers ^ " running."] - | ss => "Running " ^ workers ^ ":" :: ss - val interrupting = - case map_filter canceling_info canceling of - [] => [] - | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss - in priority (space_implode "\n\n" (running @ interrupting)) end - -fun thread_messages tool worker opt_limit = - let - val limit = the_default message_display_limit opt_limit; - val tool_store = Synchronized.value global_state - |> #store |> filter (curry (op =) tool o fst) - val header = - "Recent " ^ worker ^ " messages" ^ - (if length tool_store <= limit then ":" - else " (" ^ string_of_int limit ^ " displayed):"); - in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end - -end;