event timer as separate service thread;
authorwenzelm
Fri May 17 17:11:06 2013 +0200 (2013-05-17)
changeset 52050b40ed9dcf903
parent 52049 156e12d5cb92
child 52051 9362fcd0318c
event timer as separate service thread;
src/Pure/Concurrent/event_timer.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/session.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/event_timer.ML	Fri May 17 17:11:06 2013 +0200
     1.3 @@ -0,0 +1,129 @@
     1.4 +(*  Title:      Pure/Concurrent/event_timer.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Initiate event after given point in time.
     1.8 +
     1.9 +Note: events are run as synchronized action within a dedicated thread
    1.10 +and should finish quickly without further ado.
    1.11 +*)
    1.12 +
    1.13 +signature EVENT_TIMER =
    1.14 +sig
    1.15 +  type event = unit -> unit
    1.16 +  eqtype request
    1.17 +  val request: Time.time -> event -> request
    1.18 +  val cancel: request -> bool
    1.19 +  val shutdown: unit -> unit
    1.20 +end;
    1.21 +
    1.22 +structure Event_Timer: EVENT_TIMER =
    1.23 +struct
    1.24 +
    1.25 +(* type event *)
    1.26 +
    1.27 +type event = unit -> unit;
    1.28 +
    1.29 +
    1.30 +(* type request *)
    1.31 +
    1.32 +val request_counter = Synchronized.counter ();
    1.33 +datatype request = Request of int;
    1.34 +fun new_request () = Request (request_counter ());
    1.35 +
    1.36 +
    1.37 +(* type requests *)
    1.38 +
    1.39 +structure Requests = Table(type key = Time.time val ord = Time.compare);
    1.40 +type requests = (request * event) list Requests.table;
    1.41 +
    1.42 +fun add_request time entry (requests: requests) =
    1.43 +  Requests.cons_list (time, entry) requests;
    1.44 +
    1.45 +fun del_request req (requests: requests) =
    1.46 +  let
    1.47 +    val old_request =
    1.48 +      requests |> Requests.get_first (fn (key, entries) =>
    1.49 +        entries |> get_first (fn entry => if fst entry = req then SOME (key, entry) else NONE));
    1.50 +  in
    1.51 +    (case old_request of
    1.52 +      NONE => (false, requests)
    1.53 +    | SOME old => (true, Requests.remove_list (eq_fst op =) old requests))
    1.54 +  end;
    1.55 +
    1.56 +fun next_request_time (requests: requests) =
    1.57 +  Option.map fst (Requests.min requests);
    1.58 +
    1.59 +fun next_request_event t0 (requests: requests) =
    1.60 +  (case Requests.min requests of
    1.61 +    NONE => NONE
    1.62 +  | SOME (time, entries) =>
    1.63 +      if Time.< (t0, time) then NONE
    1.64 +      else
    1.65 +        let
    1.66 +          val (rest, (_, event)) = split_last entries;
    1.67 +          val requests' =
    1.68 +            if null rest then Requests.delete time requests
    1.69 +            else Requests.update (time, rest) requests;
    1.70 +        in SOME (event, requests') end);
    1.71 +
    1.72 +
    1.73 +(* global state *)
    1.74 +
    1.75 +type state = requests * Thread.thread option;
    1.76 +val init_state: state = (Requests.empty, NONE);
    1.77 +
    1.78 +val state = Synchronized.var "Event_Timer.state" init_state;
    1.79 +
    1.80 +
    1.81 +(* manager thread *)
    1.82 +
    1.83 +val manager_timeout = seconds 0.3;
    1.84 +
    1.85 +fun manager_loop () =
    1.86 +  let
    1.87 +    val success =
    1.88 +      Synchronized.timed_access state
    1.89 +        (fn (requests, _) =>
    1.90 +          (case next_request_time requests of
    1.91 +            NONE => SOME (Time.+ (Time.now (), manager_timeout))
    1.92 +          | some => some))
    1.93 +        (fn (requests, manager) =>
    1.94 +          (case next_request_event (Time.now ()) requests of
    1.95 +            NONE => NONE
    1.96 +          | SOME (event, requests') => (Exn.capture event (); SOME ((), (requests', manager)))));
    1.97 +    val finished =
    1.98 +      is_none success andalso
    1.99 +        Synchronized.change_result state (fn (requests, manager) =>
   1.100 +          if Requests.is_empty requests then (true, init_state)
   1.101 +          else (false, (requests, manager)));
   1.102 +  in if finished then () else manager_loop () end;
   1.103 +
   1.104 +fun manager_check manager =
   1.105 +  if is_some manager andalso Thread.isActive (the manager) then manager
   1.106 +  else SOME (Simple_Thread.fork false manager_loop);
   1.107 +
   1.108 +
   1.109 +(* main operations *)
   1.110 +
   1.111 +fun request time event =
   1.112 +  Synchronized.change_result state (fn (requests, manager) =>
   1.113 +    let
   1.114 +      val req = new_request ();
   1.115 +      val requests' = add_request time (req, event) requests;
   1.116 +    in (req, (requests', manager_check manager)) end);
   1.117 +
   1.118 +fun cancel req =
   1.119 +  Synchronized.change_result state (fn (requests, manager) =>
   1.120 +    let
   1.121 +      val (cancelled, requests') = del_request req requests;
   1.122 +    in (cancelled, (requests', manager)) end);
   1.123 +
   1.124 +fun shutdown () =
   1.125 +  Synchronized.guarded_access state (fn (requests, manager) =>
   1.126 +    if not (Requests.is_empty requests)
   1.127 +    then raise Fail "Cannot shutdown event timer: pending requests"
   1.128 +    else if is_none manager then SOME ((), init_state)
   1.129 +    else NONE);
   1.130 +
   1.131 +end;
   1.132 +
     2.1 --- a/src/Pure/ROOT	Fri May 17 13:46:18 2013 +0200
     2.2 +++ b/src/Pure/ROOT	Fri May 17 17:11:06 2013 +0200
     2.3 @@ -47,6 +47,7 @@
     2.4      "Concurrent/bash.ML"
     2.5      "Concurrent/bash_sequential.ML"
     2.6      "Concurrent/cache.ML"
     2.7 +    "Concurrent/event_timer.ML"
     2.8      "Concurrent/future.ML"
     2.9      "Concurrent/lazy.ML"
    2.10      "Concurrent/lazy_sequential.ML"
     3.1 --- a/src/Pure/ROOT.ML	Fri May 17 13:46:18 2013 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Fri May 17 17:11:06 2013 +0200
     3.3 @@ -72,6 +72,8 @@
     3.4  
     3.5  (* concurrency within the ML runtime *)
     3.6  
     3.7 +use "Concurrent/event_timer.ML";
     3.8 +
     3.9  if ML_System.is_polyml
    3.10  then use "ML/exn_properties_polyml.ML"
    3.11  else use "ML/exn_properties_dummy.ML";
     4.1 --- a/src/Pure/System/session.ML	Fri May 17 13:46:18 2013 +0200
     4.2 +++ b/src/Pure/System/session.ML	Fri May 17 17:11:06 2013 +0200
     4.3 @@ -60,6 +60,7 @@
     4.4    Outer_Syntax.check_syntax ();
     4.5    Options.reset_default ();
     4.6    Future.shutdown ();
     4.7 +  Event_Timer.shutdown ();
     4.8    session_finished := true);
     4.9  
    4.10