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
6Central manager for asynchronous diagnosis tool threads.
7
8Proof General legacy!
9*)
10
11signature ASYNC_MANAGER_LEGACY =
12sig
13  val thread : string -> Time.time -> Time.time -> string * string -> (unit -> bool * string) ->
14    unit
15  val has_running_threads : string -> bool
16end;
17
18structure Async_Manager_Legacy : ASYNC_MANAGER_LEGACY =
19struct
20
21fun 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
30fun implode_message (workers, work) =
31  space_implode " " (Try.serial_commas "and" workers) ^ work
32
33structure Thread_Heap = Heap
34(
35  type elem = Time.time * Thread.thread
36  fun ord ((a, _), (b, _)) = Time.compare (a, b)
37)
38
39fun lookup_thread xs = AList.lookup Thread.equal xs
40fun delete_thread xs = AList.delete Thread.equal xs
41fun update_thread xs = AList.update Thread.equal xs
42
43type 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
52fun make_state manager timeout_heap active canceling messages : state =
53  {manager = manager, timeout_heap = timeout_heap, active = active, canceling = canceling,
54   messages = messages}
55
56val global_state = Synchronized.var "async_manager" (make_state NONE Thread_Heap.empty [] [] [])
57
58fun 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
73val min_wait_time = seconds 0.3
74val max_wait_time = seconds 10.0
75
76fun 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
92fun 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
133fun 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
143fun 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
152fun has_running_threads tool =
153  exists (fn (_, (tool', _, _, _)) => tool' = tool) (#active (Synchronized.value global_state))
154
155end;
156