src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
author wenzelm
Sat Apr 02 23:29:05 2016 +0200 (2016-04-02 ago)
changeset 62826 eb94e570c1a4
parent 61556 0d4ee4168e41
child 63692 1bc4bc2c9fd1
permissions -rw-r--r--
prefer infix operations;
     1 (*  Title:      HOL/Tools/Sledgehammer/async_manager_legacy.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 Proof General legacy!
     9 *)
    10 
    11 signature ASYNC_MANAGER_LEGACY =
    12 sig
    13   val thread : string -> Time.time -> Time.time -> string * string -> (unit -> bool * string) ->
    14     unit
    15   val has_running_threads : string -> bool
    16 end;
    17 
    18 structure Async_Manager_Legacy : ASYNC_MANAGER_LEGACY =
    19 struct
    20 
    21 fun make_thread interrupts body =
    22   Thread.fork
    23     (fn () =>
    24       Runtime.debugging NONE body () handle exn =>
    25         if Exn.is_interrupt exn then ()
    26         else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn),
    27       Standard_Thread.attributes
    28         {name = "async_manager", stack_limit = NONE, interrupts = interrupts});
    29 
    30 fun implode_message (workers, work) =
    31   space_implode " " (Try.serial_commas "and" workers) ^ work
    32 
    33 structure Thread_Heap = Heap
    34 (
    35   type elem = Time.time * Thread.thread
    36   fun ord ((a, _), (b, _)) = Time.compare (a, b)
    37 )
    38 
    39 fun lookup_thread xs = AList.lookup Thread.equal xs
    40 fun delete_thread xs = AList.delete Thread.equal xs
    41 fun update_thread xs = AList.update Thread.equal xs
    42 
    43 type state =
    44   {manager: Thread.thread option,
    45    timeout_heap: Thread_Heap.T,
    46    active:
    47      (Thread.thread
    48       * (string * Time.time * Time.time * (string * string))) list,
    49    canceling:  (Thread.thread * (string * Time.time * (string * string))) list,
    50    messages: (bool * (string * (string * string))) list}
    51 
    52 fun make_state manager timeout_heap active canceling messages : state =
    53   {manager = manager, timeout_heap = timeout_heap, active = active, canceling = canceling,
    54    messages = messages}
    55 
    56 val global_state = Synchronized.var "async_manager" (make_state NONE Thread_Heap.empty [] [] [])
    57 
    58 fun unregister (urgent, message) thread =
    59   Synchronized.change global_state
    60   (fn state as {manager, timeout_heap, active, canceling, messages} =>
    61     (case lookup_thread active thread of
    62       SOME (tool, _, _, desc as (worker, its_desc)) =>
    63         let
    64           val active' = delete_thread thread active
    65           val now = Time.now ()
    66           val canceling' = (thread, (tool, now, desc)) :: canceling
    67           val message' =
    68             (worker, its_desc ^ (if message = "" then "" else "\n" ^ message))
    69           val messages' = (urgent, (tool, message')) :: messages
    70         in make_state manager timeout_heap active' canceling' messages' end
    71     | NONE => state))
    72 
    73 val min_wait_time = seconds 0.3
    74 val max_wait_time = seconds 10.0
    75 
    76 fun print_new_messages () =
    77   Synchronized.change_result global_state
    78       (fn {manager, timeout_heap, active, canceling, messages} =>
    79           messages
    80           |> List.partition
    81                  (fn (urgent, _) =>
    82                      (null active andalso null canceling) orelse urgent)
    83           ||> make_state manager timeout_heap active canceling)
    84   |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker))
    85   |> AList.group (op =)
    86   |> List.app (fn ((_, ""), _) => ()
    87                 | ((tool, work), workers) =>
    88                   tool ^ ": " ^
    89                   implode_message (workers |> sort_distinct string_ord, work)
    90                   |> writeln)
    91 
    92 fun check_thread_manager () = Synchronized.change global_state
    93   (fn state as {manager, timeout_heap, active, canceling, messages} =>
    94     if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
    95     else let val manager = SOME (make_thread false (fn () =>
    96       let
    97         fun time_limit timeout_heap =
    98           (case try Thread_Heap.min timeout_heap of
    99             NONE => Time.now () + max_wait_time
   100           | SOME (time, _) => time)
   101 
   102         (*action: find threads whose timeout is reached, and interrupt canceling threads*)
   103         fun action {manager, timeout_heap, active, canceling, messages} =
   104           let val (timeout_threads, timeout_heap') =
   105             Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap
   106           in
   107             if null timeout_threads andalso null canceling then
   108               NONE
   109             else
   110               let
   111                 val _ = List.app (Standard_Thread.interrupt_unsynchronized o #1) canceling
   112                 val canceling' = filter (Thread.isActive o #1) canceling
   113                 val state' = make_state manager timeout_heap' active canceling' messages
   114               in SOME (map #2 timeout_threads, state') end
   115           end
   116       in
   117         while Synchronized.change_result global_state
   118           (fn state as {timeout_heap, active, canceling, messages, ...} =>
   119             if null active andalso null canceling andalso null messages
   120             then (false, make_state NONE timeout_heap active canceling messages)
   121             else (true, state))
   122         do
   123           (Synchronized.timed_access global_state
   124                (SOME o time_limit o #timeout_heap) action
   125            |> these
   126            |> List.app (unregister (false, "Timed out."));
   127            print_new_messages ();
   128            (* give threads some time to respond to interrupt *)
   129            OS.Process.sleep min_wait_time)
   130       end))
   131     in make_state manager timeout_heap active canceling messages end)
   132 
   133 fun register tool birth_time death_time desc thread =
   134  (Synchronized.change global_state
   135     (fn {manager, timeout_heap, active, canceling, messages} =>
   136       let
   137         val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap
   138         val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active
   139         val state' = make_state manager timeout_heap' active' canceling messages
   140       in state' end);
   141   check_thread_manager ())
   142 
   143 fun thread tool birth_time death_time desc f =
   144   (make_thread true
   145        (fn () =>
   146            let
   147              val self = Thread.self ()
   148              val _ = register tool birth_time death_time desc self
   149            in unregister (f ()) self end);
   150    ())
   151 
   152 fun has_running_threads tool =
   153   exists (fn (_, (tool', _, _, _)) => tool' = tool) (#active (Synchronized.value global_state))
   154 
   155 end;