blanchet@41290: (*  Title:      HOL/Tools/Sledgehammer/async_manager.ML
blanchet@37583:     Author:     Fabian Immler, TU Muenchen
blanchet@37583:     Author:     Makarius
blanchet@37583:     Author:     Jasmin Blanchette, TU Muenchen
blanchet@37583: 
blanchet@37583: Central manager for asynchronous diagnosis tool threads.
blanchet@37583: *)
blanchet@37583: 
blanchet@37583: signature ASYNC_MANAGER =
blanchet@37583: sig
blanchet@43846:   val implode_desc : string * string -> string
blanchet@43846:   val break_into_chunks : string -> string list
blanchet@37584:   val launch :
blanchet@43846:     string -> Time.time -> Time.time -> string * string
blanchet@43846:     -> (unit -> bool * string) -> unit
blanchet@37585:   val kill_threads : string -> string -> unit
blanchet@37585:   val running_threads : string -> string -> unit
blanchet@37585:   val thread_messages : string -> string -> int option -> unit
blanchet@37583: end;
blanchet@37583: 
blanchet@37583: structure Async_Manager : ASYNC_MANAGER =
blanchet@37583: struct
blanchet@37583: 
blanchet@37583: (** preferences **)
blanchet@37583: 
blanchet@37583: val message_store_limit = 20;
blanchet@37583: val message_display_limit = 5;
blanchet@37583: 
blanchet@37583: 
blanchet@37583: (** thread management **)
blanchet@37583: 
blanchet@43846: val implode_desc = op ^ o apfst quote
blanchet@43846: 
blanchet@43846: fun implode_message (workers, work) =
blanchet@43870:   space_implode " " (Try.serial_commas "and" (map quote workers)) ^ work
blanchet@43846: 
blanchet@43846: 
blanchet@37583: (* data structures over threads *)
blanchet@37583: 
blanchet@37583: structure Thread_Heap = Heap
blanchet@37583: (
blanchet@37583:   type elem = Time.time * Thread.thread;
blanchet@37583:   fun ord ((a, _), (b, _)) = Time.compare (a, b);
blanchet@37583: );
blanchet@37583: 
blanchet@37583: fun lookup_thread xs = AList.lookup Thread.equal xs;
blanchet@37583: fun delete_thread xs = AList.delete Thread.equal xs;
blanchet@37583: fun update_thread xs = AList.update Thread.equal xs;
blanchet@37583: 
blanchet@37583: 
blanchet@37583: (* state of thread manager *)
blanchet@37583: 
blanchet@37583: type state =
blanchet@37585:   {manager: Thread.thread option,
blanchet@37585:    timeout_heap: Thread_Heap.T,
blanchet@43846:    active:
blanchet@43846:      (Thread.thread
blanchet@43846:       * (string * Time.time * Time.time * (string * string))) list,
blanchet@43846:    canceling:  (Thread.thread * (string * Time.time * (string * string))) list,
blanchet@43846:    messages: (bool * (string * (string * string))) list,
blanchet@43846:    store: (string * (string * string)) list}
blanchet@37583: 
blanchet@37583: fun make_state manager timeout_heap active canceling messages store : state =
blanchet@37583:   {manager = manager, timeout_heap = timeout_heap, active = active,
blanchet@37583:    canceling = canceling, messages = messages, store = store}
blanchet@37583: 
blanchet@37583: val global_state = Synchronized.var "async_manager"
blanchet@37583:   (make_state NONE Thread_Heap.empty [] [] [] []);
blanchet@37583: 
blanchet@37583: 
blanchet@37583: (* unregister thread *)
blanchet@37583: 
blanchet@43846: fun unregister (urgent, message) thread =
blanchet@37583:   Synchronized.change global_state
blanchet@37583:   (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
blanchet@37583:     (case lookup_thread active thread of
blanchet@43846:       SOME (tool, _, _, desc as (worker, its_desc)) =>
blanchet@37583:         let
blanchet@37583:           val active' = delete_thread thread active;
blanchet@37583:           val now = Time.now ()
blanchet@37585:           val canceling' = (thread, (tool, now, desc)) :: canceling
blanchet@43846:           val message' = (worker, its_desc ^ "\n" ^ message)
blanchet@43846:           val messages' = (urgent, (tool, message')) :: messages
blanchet@37585:           val store' = (tool, message') ::
blanchet@37583:             (if length store <= message_store_limit then store
blanchet@37583:              else #1 (chop message_store_limit store));
blanchet@37583:         in make_state manager timeout_heap active' canceling' messages' store' end
blanchet@37583:     | NONE => state));
blanchet@37583: 
blanchet@37583: 
blanchet@37583: (* main manager thread -- only one may exist *)
blanchet@37583: 
wenzelm@40553: val min_wait_time = seconds 0.3;
wenzelm@40553: val max_wait_time = seconds 10.0;
blanchet@37583: 
blanchet@37583: fun replace_all bef aft =
blanchet@37583:   let
blanchet@37583:     fun aux seen "" = String.implode (rev seen)
blanchet@37583:       | aux seen s =
blanchet@37583:         if String.isPrefix bef s then
blanchet@37583:           aux seen "" ^ aft ^ aux [] (unprefix bef s)
blanchet@37583:         else
blanchet@37583:           aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
blanchet@37583:   in aux [] end
blanchet@37583: 
blanchet@37583: (* This is a workaround for Proof General's off-by-a-few sendback display bug,
blanchet@37583:    whereby "pr" in "proof" is not highlighted. *)
blanchet@43846: val break_into_chunks = space_explode "\000" o replace_all "\n\n" "\000"
blanchet@37583: 
blanchet@37585: fun print_new_messages () =
blanchet@43846:   Synchronized.change_result global_state
blanchet@43846:       (fn {manager, timeout_heap, active, canceling, messages, store} =>
blanchet@43846:           messages
blanchet@43896:           |> List.partition
blanchet@43896:                  (fn (urgent, _) =>
blanchet@43896:                      (null active andalso null canceling) orelse urgent)
blanchet@43846:           ||> (fn postponed_messages =>
blanchet@43846:                   make_state manager timeout_heap active canceling
blanchet@43846:                                      postponed_messages store))
blanchet@43846:   |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker))
blanchet@43846:   |> AList.group (op =)
blanchet@43846:   |> List.app (fn ((tool, work), workers) =>
blanchet@43846:                   tool ^ ": " ^
blanchet@43846:                   implode_message (workers |> sort string_ord, work)
blanchet@43846:                   |> break_into_chunks
blanchet@43846:                   |> List.app Output.urgent_message)
blanchet@37583: 
blanchet@39250: fun check_thread_manager () = Synchronized.change global_state
blanchet@37583:   (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
blanchet@37583:     if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
blanchet@37583:     else let val manager = SOME (Toplevel.thread false (fn () =>
blanchet@37583:       let
blanchet@37583:         fun time_limit timeout_heap =
blanchet@37583:           (case try Thread_Heap.min timeout_heap of
blanchet@37583:             NONE => Time.+ (Time.now (), max_wait_time)
blanchet@37583:           | SOME (time, _) => time);
blanchet@37583: 
blanchet@37583:         (*action: find threads whose timeout is reached, and interrupt canceling threads*)
blanchet@37583:         fun action {manager, timeout_heap, active, canceling, messages, store} =
blanchet@37583:           let val (timeout_threads, timeout_heap') =
blanchet@37583:             Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
blanchet@37583:           in
blanchet@37585:             if null timeout_threads andalso null canceling then
blanchet@37585:               NONE
blanchet@37583:             else
blanchet@37583:               let
wenzelm@44995:                 val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling
blanchet@37583:                 val canceling' = filter (Thread.isActive o #1) canceling
blanchet@37583:                 val state' = make_state manager timeout_heap' active canceling' messages store;
blanchet@37583:               in SOME (map #2 timeout_threads, state') end
blanchet@37583:           end;
blanchet@37583:       in
blanchet@37583:         while Synchronized.change_result global_state
blanchet@37583:           (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
blanchet@37583:             if null active andalso null canceling andalso null messages
blanchet@37583:             then (false, make_state NONE timeout_heap active canceling messages store)
blanchet@37583:             else (true, state))
blanchet@37583:         do
blanchet@37583:           (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
blanchet@37583:             |> these
blanchet@43896:             |> List.app (unregister (false, "Timed out."));
blanchet@37585:             print_new_messages ();
blanchet@37583:             (*give threads some time to respond to interrupt*)
blanchet@37583:             OS.Process.sleep min_wait_time)
blanchet@37583:       end))
blanchet@37583:     in make_state manager timeout_heap active canceling messages store end)
blanchet@37583: 
blanchet@37583: 
blanchet@37583: (* register thread *)
blanchet@37583: 
blanchet@39250: fun register tool birth_time death_time desc thread =
blanchet@37583:  (Synchronized.change global_state
blanchet@37583:     (fn {manager, timeout_heap, active, canceling, messages, store} =>
blanchet@37583:       let
blanchet@37583:         val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
blanchet@37585:         val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
blanchet@37583:         val state' = make_state manager timeout_heap' active' canceling messages store;
blanchet@37583:       in state' end);
blanchet@39250:   check_thread_manager ())
blanchet@37583: 
blanchet@37583: 
blanchet@39250: fun launch tool birth_time death_time desc f =
blanchet@37584:   (Toplevel.thread true
blanchet@37584:        (fn () =>
blanchet@37584:            let
blanchet@37584:              val self = Thread.self ()
blanchet@39250:              val _ = register tool birth_time death_time desc self
blanchet@43846:            in unregister (f ()) self end);
blanchet@37584:    ())
blanchet@37584: 
blanchet@37583: 
blanchet@37583: (** user commands **)
blanchet@37583: 
blanchet@37583: (* kill threads *)
blanchet@37583: 
blanchet@43846: fun kill_threads tool das_wort_worker = Synchronized.change global_state
blanchet@37583:   (fn {manager, timeout_heap, active, canceling, messages, store} =>
blanchet@37583:     let
blanchet@37585:       val killing =
blanchet@37585:         map_filter (fn (th, (tool', _, _, desc)) =>
blanchet@37585:                        if tool' = tool then SOME (th, (tool', Time.now (), desc))
blanchet@37585:                        else NONE) active
blanchet@37583:       val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
blanchet@43846:       val _ =
blanchet@43846:         if null killing then ()
blanchet@46444:         else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.")
blanchet@37583:     in state' end);
blanchet@37583: 
blanchet@37583: 
blanchet@37583: (* running threads *)
blanchet@37583: 
blanchet@37585: fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
blanchet@37583: 
blanchet@43846: fun running_threads tool das_wort_worker =
blanchet@37583:   let
blanchet@37583:     val {active, canceling, ...} = Synchronized.value global_state;
blanchet@37583: 
blanchet@37583:     val now = Time.now ();
blanchet@37585:     fun running_info (_, (tool', birth_time, death_time, desc)) =
blanchet@37585:       if tool' = tool then
blanchet@37585:         SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
blanchet@43846:               seconds (Time.- (death_time, now)) ^ " to live:\n" ^
blanchet@43846:               implode_desc desc)
blanchet@37585:       else
blanchet@37585:         NONE
blanchet@37585:     fun canceling_info (_, (tool', death_time, desc)) =
blanchet@37585:       if tool' = tool then
blanchet@43846:         SOME ("Trying to interrupt " ^ das_wort_worker ^ " since " ^
blanchet@43846:               seconds (Time.- (now, death_time)) ^ ":\n" ^ implode_desc desc)
blanchet@37585:       else
blanchet@37585:         NONE
blanchet@37583:     val running =
blanchet@37585:       case map_filter running_info active of
blanchet@43846:         [] => ["No " ^ das_wort_worker ^ "s running."]
blanchet@43846:       | ss => "Running " ^ das_wort_worker ^ "s " :: ss
blanchet@37583:     val interrupting =
blanchet@37585:       case map_filter canceling_info canceling of
blanchet@37583:         [] => []
blanchet@43846:       | ss => "Interrupting " ^ das_wort_worker ^ "s " :: ss
wenzelm@40392:   in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
blanchet@37583: 
blanchet@43846: fun thread_messages tool das_wort_worker opt_limit =
blanchet@37583:   let
blanchet@37583:     val limit = the_default message_display_limit opt_limit;
blanchet@37585:     val tool_store = Synchronized.value global_state
blanchet@37585:                      |> #store |> filter (curry (op =) tool o fst)
blanchet@37583:     val header =
blanchet@43846:       "Recent " ^ das_wort_worker ^ " messages" ^
blanchet@37585:         (if length tool_store <= limit then ":"
blanchet@37585:          else " (" ^ string_of_int limit ^ " displayed):");
blanchet@43846:     val ss = tool_store |> chop limit |> #1 |> map (implode_desc o snd)
blanchet@43846:   in List.app Output.urgent_message (header :: maps break_into_chunks ss) end
blanchet@37583: 
blanchet@37583: end;