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