1.1 --- a/src/HOL/Tools/atp_manager.ML Wed Apr 01 11:46:17 2009 +0200
1.2 +++ b/src/HOL/Tools/atp_manager.ML Wed Apr 01 11:53:59 2009 +0200
1.3 @@ -85,36 +85,25 @@
1.4 (* state of thread manager *)
1.5
1.6 datatype T = State of
1.7 - {timeout_heap: ThreadHeap.T,
1.8 + {managing_thread: Thread.thread option,
1.9 + timeout_heap: ThreadHeap.T,
1.10 oldest_heap: ThreadHeap.T,
1.11 active: (Thread.thread * (Time.time * Time.time * string)) list,
1.12 cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
1.13 messages: string list,
1.14 store: string list};
1.15
1.16 -fun make_state timeout_heap oldest_heap active cancelling messages store =
1.17 - State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
1.18 +fun make_state managing_thread timeout_heap oldest_heap active cancelling messages store =
1.19 + State {managing_thread = managing_thread, timeout_heap = timeout_heap, oldest_heap = oldest_heap,
1.20 active = active, cancelling = cancelling, messages = messages, store = store};
1.21
1.22 -fun empty_state state =
1.23 - let
1.24 - val State {active = active, cancelling = cancelling, messages = messages, ...} =
1.25 - Synchronized.value state
1.26 - in (null active) andalso (null cancelling) andalso (null messages) end;
1.27 -
1.28 -val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] [] []);
1.29 -
1.30 -
1.31 -(* the managing thread *)
1.32 -
1.33 -(*watches over running threads and interrupts them if required*)
1.34 -val managing_thread = ref (NONE: Thread.thread option);
1.35 -
1.36 +val state = Synchronized.var "atp_manager"
1.37 + (make_state NONE ThreadHeap.empty ThreadHeap.empty [] [] [] []);
1.38
1.39 (* unregister thread *)
1.40
1.41 fun unregister (success, message) thread = Synchronized.change state
1.42 - (fn state as State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
1.43 + (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
1.44 (case lookup_thread active thread of
1.45 SOME (birthtime, _, description) =>
1.46 let
1.47 @@ -132,7 +121,9 @@
1.48 val store' = message' ::
1.49 (if length store <= message_store_limit then store
1.50 else #1 (chop message_store_limit store))
1.51 - in make_state timeout_heap oldest_heap active' cancelling' (message' :: messages) store' end
1.52 + in make_state
1.53 + managing_thread timeout_heap oldest_heap active' cancelling' (message' :: messages) store'
1.54 + end
1.55 | NONE => state));
1.56
1.57
1.58 @@ -147,12 +138,13 @@
1.59 fun kill_oldest () =
1.60 let exception Unchanged in
1.61 Synchronized.change_result state
1.62 - (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
1.63 + (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
1.64 if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
1.65 then raise Unchanged
1.66 else
1.67 let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
1.68 - in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages store) end)
1.69 + in (oldest_thread,
1.70 + make_state managing_thread timeout_heap oldest_heap' active cancelling messages store) end)
1.71 |> unregister (false, "Interrupted (maximum number of ATPs exceeded)")
1.72 handle Unchanged => ()
1.73 end;
1.74 @@ -167,8 +159,8 @@
1.75
1.76 fun print_new_messages () =
1.77 let val to_print = Synchronized.change_result state
1.78 - (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
1.79 - (messages, make_state timeout_heap oldest_heap active cancelling [] store))
1.80 + (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
1.81 + (messages, make_state managing_thread timeout_heap oldest_heap active cancelling [] store))
1.82 in
1.83 if null to_print then ()
1.84 else priority ("Sledgehammer: " ^ space_implode "\n\n" to_print)
1.85 @@ -177,55 +169,66 @@
1.86
1.87 (* start a watching thread -- only one may exist *)
1.88
1.89 -fun check_thread_manager () = CRITICAL (fn () =>
1.90 - if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false)
1.91 - then () else managing_thread := SOME (SimpleThread.fork false (fn () =>
1.92 - let
1.93 - val min_wait_time = Time.fromMilliseconds 300
1.94 - val max_wait_time = Time.fromSeconds 10
1.95 +fun check_thread_manager () = Synchronized.change state
1.96 + (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
1.97 + if (case managing_thread of SOME thread => Thread.isActive thread | NONE => false)
1.98 + then make_state managing_thread timeout_heap oldest_heap active cancelling messages store
1.99 + else let val managing_thread = SOME (SimpleThread.fork false (fn () =>
1.100 + let
1.101 + val min_wait_time = Time.fromMilliseconds 300
1.102 + val max_wait_time = Time.fromSeconds 10
1.103
1.104 - (* wait for next thread to cancel, or maximum*)
1.105 - fun time_limit (State {timeout_heap, ...}) =
1.106 - (case try ThreadHeap.min timeout_heap of
1.107 - NONE => SOME (Time.+ (Time.now (), max_wait_time))
1.108 - | SOME (time, _) => SOME time)
1.109 + (* wait for next thread to cancel, or maximum*)
1.110 + fun time_limit (State {timeout_heap, ...}) =
1.111 + (case try ThreadHeap.min timeout_heap of
1.112 + NONE => SOME (Time.+ (Time.now (), max_wait_time))
1.113 + | SOME (time, _) => SOME time)
1.114
1.115 - (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
1.116 - fun action (State {timeout_heap, oldest_heap, active, cancelling, messages, store}) =
1.117 - let val (timeout_threads, timeout_heap') =
1.118 - ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
1.119 - in
1.120 - if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
1.121 - then NONE
1.122 - else
1.123 - let
1.124 - val _ = List.app (SimpleThread.interrupt o #1) cancelling
1.125 - val cancelling' = filter (Thread.isActive o #1) cancelling
1.126 - val state' = make_state timeout_heap' oldest_heap active cancelling' messages store
1.127 - in SOME (map #2 timeout_threads, state') end
1.128 - end
1.129 - in
1.130 - while not (empty_state state) do
1.131 - (Synchronized.timed_access state time_limit action
1.132 - |> these
1.133 - |> List.app (unregister (false, "Interrupted (reached timeout)"));
1.134 - kill_excessive ();
1.135 - print_new_messages ();
1.136 - (*give threads time to respond to interrupt*)
1.137 - OS.Process.sleep min_wait_time)
1.138 - end)));
1.139 + (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
1.140 + fun action (State {managing_thread, timeout_heap, oldest_heap, active, cancelling,
1.141 + messages, store}) =
1.142 + let val (timeout_threads, timeout_heap') =
1.143 + ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
1.144 + in
1.145 + if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
1.146 + then NONE
1.147 + else
1.148 + let
1.149 + val _ = List.app (SimpleThread.interrupt o #1) cancelling
1.150 + val cancelling' = filter (Thread.isActive o #1) cancelling
1.151 + val state' = make_state
1.152 + managing_thread timeout_heap' oldest_heap active cancelling' messages store
1.153 + in SOME (map #2 timeout_threads, state') end
1.154 + end
1.155 + in
1.156 + while Synchronized.change_result state
1.157 + (fn st as
1.158 + State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
1.159 + if (null active) andalso (null cancelling) andalso (null messages)
1.160 + then (false, make_state NONE timeout_heap oldest_heap active cancelling messages store)
1.161 + else (true, st))
1.162 + do
1.163 + (Synchronized.timed_access state time_limit action
1.164 + |> these
1.165 + |> List.app (unregister (false, "Interrupted (reached timeout)"));
1.166 + kill_excessive ();
1.167 + print_new_messages ();
1.168 + (*give threads time to respond to interrupt*)
1.169 + OS.Process.sleep min_wait_time)
1.170 + end))
1.171 + in make_state managing_thread timeout_heap oldest_heap active cancelling messages store end);
1.172
1.173
1.174 (* thread is registered here by sledgehammer *)
1.175
1.176 fun register birthtime deadtime (thread, desc) =
1.177 (Synchronized.change state
1.178 - (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
1.179 + (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
1.180 let
1.181 val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
1.182 val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
1.183 val active' = update_thread (thread, (birthtime, deadtime, desc)) active
1.184 - in make_state timeout_heap' oldest_heap' active' cancelling messages store end);
1.185 + in make_state managing_thread timeout_heap' oldest_heap' active' cancelling messages store end);
1.186 check_thread_manager ());
1.187
1.188
1.189 @@ -235,9 +238,11 @@
1.190 (* kill: move all threads to cancelling *)
1.191
1.192 fun kill () = Synchronized.change state
1.193 - (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
1.194 + (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
1.195 let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
1.196 - in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store end);
1.197 + in make_state
1.198 + managing_thread timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store
1.199 + end);
1.200
1.201
1.202 (* ATP info *)