src/Pure/Concurrent/synchronized.ML
author wenzelm
Mon, 13 Oct 2008 15:48:40 +0200
changeset 28578 c7f2a0899679
child 28580 3f37ae257506
permissions -rw-r--r--
State variables with synchronized access.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/synchronized.ML
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     3
    Author:     Fabian Immler and Makarius
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     4
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     5
State variables with synchronized access.
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     6
*)
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     7
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     8
signature SYNCHRONIZED =
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     9
sig
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    10
  type 'a var
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    11
  val var: string -> 'a -> 'a var
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    12
  val guarded_change: ('a -> bool) -> ('a -> Time.time option) ->
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    13
    'a var -> (bool -> 'a -> 'b * 'a) -> 'b
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    14
  val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    15
  val change: 'a var -> ('a -> 'a) -> unit
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    16
end;
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    17
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    18
structure Synchronized: SYNCHRONIZED =
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    19
struct
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    20
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    21
(* state variables *)
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    22
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    23
datatype 'a var = Var of
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    24
 {name: string,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    25
  lock: Mutex.mutex,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    26
  cond: ConditionVar.conditionVar,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    27
  var: 'a ref};
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    28
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    29
fun var name x = Var
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    30
 {name = name,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    31
  lock = Mutex.mutex (),
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    32
  cond = ConditionVar.conditionVar (),
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    33
  var = ref x};
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    34
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    35
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    36
(* synchronized access *)
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    37
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    38
fun guarded_change guard time_limit (Var {name, lock, cond, var}) f =
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    39
  SimpleThread.synchronized name lock (fn () =>
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    40
    let
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    41
      fun check () = guard (! var) orelse
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    42
        (case time_limit (! var) of
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    43
          NONE => (ConditionVar.wait (cond, lock); check ())
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    44
        | SOME t => ConditionVar.waitUntil (cond, lock, t) andalso check ());
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    45
      val ok = check ();
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    46
      val res = change_result var (f ok);
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    47
      val _ = ConditionVar.broadcast cond;
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    48
    in res end);
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    49
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    50
fun change_result var f = guarded_change (K true) (K NONE) var (K f);
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    51
fun change var f = change_result var (fn x => ((), f x));
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    52
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    53
end;