src/Pure/Concurrent/event_timer.ML
author hoelzl
Wed, 02 Apr 2014 18:35:01 +0200
changeset 56369 2704ca85be98
parent 52798 9d3c9862d1dd
child 56768 06388a5cfb7c
permissions -rw-r--r--
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52050
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/event_timer.ML
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
     3
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
     4
Initiate event after given point in time.
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
     5
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
     6
Note: events are run as synchronized action within a dedicated thread
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
     7
and should finish quickly without further ado.
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
     8
*)
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
     9
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    10
signature EVENT_TIMER =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    11
sig
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    12
  type event = unit -> unit
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    13
  eqtype request
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    14
  val request: Time.time -> event -> request
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    15
  val cancel: request -> bool
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    16
  val shutdown: unit -> unit
52798
9d3c9862d1dd recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents: 52589
diff changeset
    17
  val future: Time.time -> unit future
52050
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    18
end;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    19
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    20
structure Event_Timer: EVENT_TIMER =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    21
struct
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    22
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    23
(* type event *)
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    24
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    25
type event = unit -> unit;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    26
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    27
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    28
(* type request *)
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    29
52537
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents: 52050
diff changeset
    30
val request_counter = Counter.make ();
52050
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    31
datatype request = Request of int;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    32
fun new_request () = Request (request_counter ());
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    33
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    34
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    35
(* type requests *)
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    36
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    37
structure Requests = Table(type key = Time.time val ord = Time.compare);
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    38
type requests = (request * event) list Requests.table;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    39
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    40
fun add_request time entry (requests: requests) =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    41
  Requests.cons_list (time, entry) requests;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    42
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    43
fun del_request req (requests: requests) =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    44
  let
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    45
    val old_request =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    46
      requests |> Requests.get_first (fn (key, entries) =>
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    47
        entries |> get_first (fn entry => if fst entry = req then SOME (key, entry) else NONE));
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    48
  in
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    49
    (case old_request of
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    50
      NONE => (false, requests)
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    51
    | SOME old => (true, Requests.remove_list (eq_fst op =) old requests))
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    52
  end;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    53
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    54
fun next_request_time (requests: requests) =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    55
  Option.map fst (Requests.min requests);
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    56
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    57
fun next_request_event t0 (requests: requests) =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    58
  (case Requests.min requests of
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    59
    NONE => NONE
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    60
  | SOME (time, entries) =>
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    61
      if Time.< (t0, time) then NONE
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    62
      else
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    63
        let
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    64
          val (rest, (_, event)) = split_last entries;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    65
          val requests' =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    66
            if null rest then Requests.delete time requests
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    67
            else Requests.update (time, rest) requests;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    68
        in SOME (event, requests') end);
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    69
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    70
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    71
(* global state *)
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    72
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    73
type state = requests * Thread.thread option;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    74
val init_state: state = (Requests.empty, NONE);
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    75
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    76
val state = Synchronized.var "Event_Timer.state" init_state;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    77
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    78
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    79
(* manager thread *)
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    80
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    81
val manager_timeout = seconds 0.3;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    82
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    83
fun manager_loop () =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    84
  let
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    85
    val success =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    86
      Synchronized.timed_access state
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    87
        (fn (requests, _) =>
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    88
          (case next_request_time requests of
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    89
            NONE => SOME (Time.+ (Time.now (), manager_timeout))
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    90
          | some => some))
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    91
        (fn (requests, manager) =>
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    92
          (case next_request_event (Time.now ()) requests of
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    93
            NONE => NONE
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    94
          | SOME (event, requests') => (Exn.capture event (); SOME ((), (requests', manager)))));
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    95
    val finished =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    96
      is_none success andalso
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    97
        Synchronized.change_result state (fn (requests, manager) =>
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    98
          if Requests.is_empty requests then (true, init_state)
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
    99
          else (false, (requests, manager)));
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   100
  in if finished then () else manager_loop () end;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   101
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   102
fun manager_check manager =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   103
  if is_some manager andalso Thread.isActive (the manager) then manager
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   104
  else SOME (Simple_Thread.fork false manager_loop);
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   105
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   106
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   107
(* main operations *)
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   108
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   109
fun request time event =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   110
  Synchronized.change_result state (fn (requests, manager) =>
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   111
    let
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   112
      val req = new_request ();
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   113
      val requests' = add_request time (req, event) requests;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   114
    in (req, (requests', manager_check manager)) end);
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   115
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   116
fun cancel req =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   117
  Synchronized.change_result state (fn (requests, manager) =>
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   118
    let
52589
wenzelm
parents: 52537
diff changeset
   119
      val (canceled, requests') = del_request req requests;
wenzelm
parents: 52537
diff changeset
   120
    in (canceled, (requests', manager)) end);
52050
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   121
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   122
fun shutdown () =
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   123
  Synchronized.guarded_access state (fn (requests, manager) =>
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   124
    if not (Requests.is_empty requests)
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   125
    then raise Fail "Cannot shutdown event timer: pending requests"
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   126
    else if is_none manager then SOME ((), init_state)
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   127
    else NONE);
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   128
52798
9d3c9862d1dd recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents: 52589
diff changeset
   129
9d3c9862d1dd recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents: 52589
diff changeset
   130
(* future *)
9d3c9862d1dd recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents: 52589
diff changeset
   131
9d3c9862d1dd recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents: 52589
diff changeset
   132
val future = uninterruptible (fn _ => fn time =>
9d3c9862d1dd recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents: 52589
diff changeset
   133
  let
9d3c9862d1dd recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents: 52589
diff changeset
   134
    val req: request Single_Assignment.var = Single_Assignment.var "request";
9d3c9862d1dd recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents: 52589
diff changeset
   135
    fun abort () = ignore (cancel (Single_Assignment.await req));
9d3c9862d1dd recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents: 52589
diff changeset
   136
    val promise: unit future = Future.promise abort;
9d3c9862d1dd recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents: 52589
diff changeset
   137
    val _ = Single_Assignment.assign req (request time (Future.fulfill promise));
9d3c9862d1dd recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents: 52589
diff changeset
   138
  in promise end);
9d3c9862d1dd recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents: 52589
diff changeset
   139
52050
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   140
end;
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents:
diff changeset
   141