# HG changeset patch # User wenzelm # Date 1420827600 -3600 # Node ID 72278d083d3a2b03f9f2ccb9333b9f77755082ac # Parent b83d6c3c439a2c84eacde2c5c8b5c851836f7a01 clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish; discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage; diff -r b83d6c3c439a -r 72278d083d3a src/Pure/Concurrent/event_timer.ML --- a/src/Pure/Concurrent/event_timer.ML Fri Jan 09 11:51:02 2015 +0100 +++ b/src/Pure/Concurrent/event_timer.ML Fri Jan 09 19:20:00 2015 +0100 @@ -64,34 +64,38 @@ (* global state *) -type state = requests * Thread.thread option; -val init_state: state = (Requests.empty, NONE); +datatype status = Normal | Shutdown_Req | Shutdown_Ack; + +datatype state = + State of {requests: requests, status: status, manager: Thread.thread option}; + +fun make_state (requests, status, manager) = + State {requests = requests, status = status, manager = manager}; -val state = Synchronized.var "Event_Timer.state" init_state; +val normal_state = make_state (Requests.empty, Normal, NONE); +val shutdown_ack_state = make_state (Requests.empty, Shutdown_Ack, NONE); + +fun is_shutdown s (State {requests, status, manager}) = + Requests.is_empty requests andalso status = s andalso is_none manager; + +fun is_shutdown_req (State {requests, status, ...}) = + Requests.is_empty requests andalso status = Shutdown_Req; + +val state = Synchronized.var "Event_Timer.state" normal_state; (* manager thread *) -val manager_timeout = seconds 0.3; - fun manager_loop () = - let - val success = - Synchronized.timed_access state - (fn (requests, _) => - (case next_request_time requests of - NONE => SOME (Time.+ (Time.now (), manager_timeout)) - | some => some)) - (fn (requests, manager) => - (case next_request_event (Time.now ()) requests of - NONE => NONE - | SOME (event, requests') => (Exn.capture event (); SOME ((), (requests', manager))))); - val finished = - is_none success andalso - Synchronized.change_result state (fn (requests, manager) => - if Requests.is_empty requests then (true, init_state) - else (false, (requests, manager))); - in if finished then () else manager_loop () end; + if Synchronized.timed_access state + (fn State {requests, ...} => next_request_time requests) + (fn st as State {requests, status, manager} => + (case next_request_event (Time.now ()) requests of + SOME (event, requests') => + (Exn.capture event (); SOME (true, make_state (requests', status, manager))) + | NONE => + if is_shutdown_req st then SOME (false, shutdown_ack_state) else NONE)) = SOME false + then () else manager_loop (); fun manager_check manager = if is_some manager andalso Thread.isActive (the manager) then manager @@ -101,24 +105,35 @@ (* main operations *) fun request time event = - Synchronized.change_result state (fn (requests, manager) => + Synchronized.change_result state (fn State {requests, status, manager} => let val req = new_request (); val requests' = add_request time (req, event) requests; - in (req, (requests', manager_check manager)) end); + in (req, make_state (requests', status, manager_check manager)) end); fun cancel req = - Synchronized.change_result state (fn (requests, manager) => + Synchronized.change_result state (fn State {requests, status, manager} => let val (canceled, requests') = del_request req requests; - in (canceled, (requests', manager)) end); + in (canceled, make_state (requests', status, manager_check manager)) end); fun shutdown () = - Synchronized.guarded_access state (fn (requests, manager) => - if not (Requests.is_empty requests) - then raise Fail "Cannot shutdown event timer: pending requests" - else if is_none manager then SOME ((), init_state) - else NONE); + uninterruptible (fn restore_attributes => fn () => + if Synchronized.change_result state (fn st as State {requests, status, manager} => + if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then + raise Fail "Concurrent attempt to shutdown event timer" + else if is_shutdown Normal st then (false, st) + else (true, make_state (requests, Shutdown_Req, manager_check manager))) + then + restore_attributes (fn () => + Synchronized.guarded_access state + (fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE)) () + handle exn => + if Exn.is_interrupt exn then + Synchronized.change state (fn State {requests, manager, ...} => + make_state (requests, Normal, manager)) + else () + else ()) (); (* future *)