src/HOL/Tools/Sledgehammer/async_manager.ML
author blanchet
Sun May 01 18:37:23 2011 +0200 (2011-05-01)
changeset 42520 d1f7c4a01dbe
parent 41042 8275f52ac991
child 43005 c96f06bffd90
permissions -rw-r--r--
renamings
     1 (*  Title:      HOL/Tools/Sledgehammer/async_manager.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 
     9 signature ASYNC_MANAGER =
    10 sig
    11   val break_into_chunks : string list -> string list
    12   val launch :
    13     string -> Time.time -> Time.time -> string -> (unit -> string) -> unit
    14   val kill_threads : string -> string -> unit
    15   val running_threads : string -> string -> unit
    16   val thread_messages : string -> string -> int option -> unit
    17 end;
    18 
    19 structure Async_Manager : ASYNC_MANAGER =
    20 struct
    21 
    22 (** preferences **)
    23 
    24 val message_store_limit = 20;
    25 val message_display_limit = 5;
    26 
    27 
    28 (** thread management **)
    29 
    30 (* data structures over threads *)
    31 
    32 structure Thread_Heap = Heap
    33 (
    34   type elem = Time.time * Thread.thread;
    35   fun ord ((a, _), (b, _)) = Time.compare (a, b);
    36 );
    37 
    38 fun lookup_thread xs = AList.lookup Thread.equal xs;
    39 fun delete_thread xs = AList.delete Thread.equal xs;
    40 fun update_thread xs = AList.update Thread.equal xs;
    41 
    42 
    43 (* state of thread manager *)
    44 
    45 type state =
    46   {manager: Thread.thread option,
    47    timeout_heap: Thread_Heap.T,
    48    active: (Thread.thread * (string * Time.time * Time.time * string)) list,
    49    canceling: (Thread.thread * (string * Time.time * string)) list,
    50    messages: (string * string) list,
    51    store: (string * string) list}
    52 
    53 fun make_state manager timeout_heap active canceling messages store : state =
    54   {manager = manager, timeout_heap = timeout_heap, active = active,
    55    canceling = canceling, messages = messages, store = store}
    56 
    57 val global_state = Synchronized.var "async_manager"
    58   (make_state NONE Thread_Heap.empty [] [] [] []);
    59 
    60 
    61 (* unregister thread *)
    62 
    63 fun unregister message thread =
    64   Synchronized.change global_state
    65   (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
    66     (case lookup_thread active thread of
    67       SOME (tool, _, _, desc) =>
    68         let
    69           val active' = delete_thread thread active;
    70           val now = Time.now ()
    71           val canceling' = (thread, (tool, now, desc)) :: canceling
    72           val message' = desc ^ "\n" ^ message
    73           val messages' = (tool, message') :: messages;
    74           val store' = (tool, message') ::
    75             (if length store <= message_store_limit then store
    76              else #1 (chop message_store_limit store));
    77         in make_state manager timeout_heap active' canceling' messages' store' end
    78     | NONE => state));
    79 
    80 
    81 (* main manager thread -- only one may exist *)
    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,
    97    whereby "pr" in "proof" is not highlighted. *)
    98 val break_into_chunks = maps (space_explode "\000" o replace_all "\n\n" "\000")
    99 
   100 fun print_new_messages () =
   101   case Synchronized.change_result global_state
   102          (fn {manager, timeout_heap, active, canceling, messages, store} =>
   103              (messages, make_state manager timeout_heap active canceling []
   104                                    store)) of
   105     [] => ()
   106   | msgs as (tool, _) :: _ =>
   107     let val ss = break_into_chunks (map snd msgs) in
   108       List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss)
   109     end
   110 
   111 fun check_thread_manager () = Synchronized.change global_state
   112   (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
   113     if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
   114     else let val manager = SOME (Toplevel.thread false (fn () =>
   115       let
   116         fun time_limit timeout_heap =
   117           (case try Thread_Heap.min timeout_heap of
   118             NONE => Time.+ (Time.now (), max_wait_time)
   119           | SOME (time, _) => time);
   120 
   121         (*action: find threads whose timeout is reached, and interrupt canceling threads*)
   122         fun action {manager, timeout_heap, active, canceling, messages, store} =
   123           let val (timeout_threads, timeout_heap') =
   124             Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
   125           in
   126             if null timeout_threads andalso null canceling then
   127               NONE
   128             else
   129               let
   130                 val _ = List.app (Simple_Thread.interrupt o #1) canceling
   131                 val canceling' = filter (Thread.isActive o #1) canceling
   132                 val state' = make_state manager timeout_heap' active canceling' messages store;
   133               in SOME (map #2 timeout_threads, state') end
   134           end;
   135       in
   136         while Synchronized.change_result global_state
   137           (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
   138             if null active andalso null canceling andalso null messages
   139             then (false, make_state NONE timeout_heap active canceling messages store)
   140             else (true, state))
   141         do
   142           (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
   143             |> these
   144             |> List.app (unregister "Timed out.\n");
   145             print_new_messages ();
   146             (*give threads some time to respond to interrupt*)
   147             OS.Process.sleep min_wait_time)
   148       end))
   149     in make_state manager timeout_heap active canceling messages store end)
   150 
   151 
   152 (* register thread *)
   153 
   154 fun register tool birth_time death_time desc thread =
   155  (Synchronized.change global_state
   156     (fn {manager, timeout_heap, active, canceling, messages, store} =>
   157       let
   158         val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
   159         val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
   160         val state' = make_state manager timeout_heap' active' canceling messages store;
   161       in state' end);
   162   check_thread_manager ())
   163 
   164 
   165 fun launch tool birth_time death_time desc f =
   166   (Toplevel.thread true
   167        (fn () =>
   168            let
   169              val self = Thread.self ()
   170              val _ = register tool birth_time death_time desc self
   171              val message = f ()
   172            in unregister message self end);
   173    ())
   174 
   175 
   176 (** user commands **)
   177 
   178 (* kill threads *)
   179 
   180 fun kill_threads tool workers = Synchronized.change global_state
   181   (fn {manager, timeout_heap, active, canceling, messages, store} =>
   182     let
   183       val killing =
   184         map_filter (fn (th, (tool', _, _, desc)) =>
   185                        if tool' = tool then SOME (th, (tool', Time.now (), desc))
   186                        else NONE) active
   187       val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
   188       val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".")
   189     in state' end);
   190 
   191 
   192 (* running threads *)
   193 
   194 fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
   195 
   196 fun running_threads tool workers =
   197   let
   198     val {active, canceling, ...} = Synchronized.value global_state;
   199 
   200     val now = Time.now ();
   201     fun running_info (_, (tool', birth_time, death_time, desc)) =
   202       if tool' = tool then
   203         SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
   204               seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
   205       else
   206         NONE
   207     fun canceling_info (_, (tool', death_time, desc)) =
   208       if tool' = tool then
   209         SOME ("Trying to interrupt thread since " ^
   210               seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
   211       else
   212         NONE
   213     val running =
   214       case map_filter running_info active of
   215         [] => ["No " ^ workers ^ " running."]
   216       | ss => "Running " ^ workers ^ ":" :: ss
   217     val interrupting =
   218       case map_filter canceling_info canceling of
   219         [] => []
   220       | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
   221   in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
   222 
   223 fun thread_messages tool 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 " ^ worker ^ " messages" ^
   230         (if length tool_store <= limit then ":"
   231          else " (" ^ string_of_int limit ^ " displayed):");
   232   in
   233     List.app Output.urgent_message (header :: break_into_chunks
   234                                      (map snd (#1 (chop limit tool_store))))
   235   end
   236 
   237 end;