src/Pure/Concurrent/synchronized.ML
author wenzelm
Tue Oct 14 13:01:56 2008 +0200 (2008-10-14)
changeset 28580 3f37ae257506
parent 28578 c7f2a0899679
child 29564 f8b933a62151
permissions -rw-r--r--
added value;
simplified synchronized variable access;
wenzelm@28578
     1
(*  Title:      Pure/Concurrent/synchronized.ML
wenzelm@28578
     2
    ID:         $Id$
wenzelm@28578
     3
    Author:     Fabian Immler and Makarius
wenzelm@28578
     4
wenzelm@28578
     5
State variables with synchronized access.
wenzelm@28578
     6
*)
wenzelm@28578
     7
wenzelm@28578
     8
signature SYNCHRONIZED =
wenzelm@28578
     9
sig
wenzelm@28578
    10
  type 'a var
wenzelm@28578
    11
  val var: string -> 'a -> 'a var
wenzelm@28580
    12
  val value: 'a var -> 'a
wenzelm@28580
    13
  val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
wenzelm@28580
    14
  val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
wenzelm@28578
    15
  val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
wenzelm@28578
    16
  val change: 'a var -> ('a -> 'a) -> unit
wenzelm@28578
    17
end;
wenzelm@28578
    18
wenzelm@28578
    19
structure Synchronized: SYNCHRONIZED =
wenzelm@28578
    20
struct
wenzelm@28578
    21
wenzelm@28578
    22
(* state variables *)
wenzelm@28578
    23
wenzelm@28578
    24
datatype 'a var = Var of
wenzelm@28578
    25
 {name: string,
wenzelm@28578
    26
  lock: Mutex.mutex,
wenzelm@28578
    27
  cond: ConditionVar.conditionVar,
wenzelm@28578
    28
  var: 'a ref};
wenzelm@28578
    29
wenzelm@28578
    30
fun var name x = Var
wenzelm@28578
    31
 {name = name,
wenzelm@28578
    32
  lock = Mutex.mutex (),
wenzelm@28578
    33
  cond = ConditionVar.conditionVar (),
wenzelm@28578
    34
  var = ref x};
wenzelm@28578
    35
wenzelm@28580
    36
fun value (Var {name, lock, cond, var}) = SimpleThread.synchronized name lock (fn () => ! var);
wenzelm@28580
    37
wenzelm@28578
    38
wenzelm@28578
    39
(* synchronized access *)
wenzelm@28578
    40
wenzelm@28580
    41
fun timed_access (Var {name, lock, cond, var}) time_limit f =
wenzelm@28578
    42
  SimpleThread.synchronized name lock (fn () =>
wenzelm@28578
    43
    let
wenzelm@28580
    44
      fun try_change () =
wenzelm@28580
    45
        let val x = ! var in
wenzelm@28580
    46
          (case f x of
wenzelm@28580
    47
            SOME (y, x') => (var := x'; SOME y)
wenzelm@28580
    48
          | NONE =>
wenzelm@28580
    49
              (case time_limit x of
wenzelm@28580
    50
                NONE => (ConditionVar.wait (cond, lock); try_change ())
wenzelm@28580
    51
              | SOME t =>
wenzelm@28580
    52
                  if ConditionVar.waitUntil (cond, lock, t) then try_change ()
wenzelm@28580
    53
                  else NONE))
wenzelm@28580
    54
        end;
wenzelm@28580
    55
      val res = try_change ();
wenzelm@28578
    56
      val _ = ConditionVar.broadcast cond;
wenzelm@28578
    57
    in res end);
wenzelm@28578
    58
wenzelm@28580
    59
fun guarded_access var f = the (timed_access var (K NONE) f);
wenzelm@28580
    60
wenzelm@28580
    61
wenzelm@28580
    62
(* unconditional change *)
wenzelm@28580
    63
wenzelm@28580
    64
fun change_result var f = guarded_access var (SOME o f);
wenzelm@28578
    65
fun change var f = change_result var (fn x => ((), f x));
wenzelm@28578
    66
wenzelm@28578
    67
end;