src/Pure/Concurrent/synchronized.ML
author wenzelm
Tue Sep 29 11:49:22 2009 +0200 (2009-09-29)
changeset 32738 15bb09ca0378
parent 32592 e29c0b7dcf66
child 33060 e66b41782cb5
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
wenzelm@28578
     1
(*  Title:      Pure/Concurrent/synchronized.ML
wenzelm@28578
     2
    Author:     Fabian Immler and Makarius
wenzelm@28578
     3
wenzelm@28578
     4
State variables with synchronized access.
wenzelm@28578
     5
*)
wenzelm@28578
     6
wenzelm@28578
     7
signature SYNCHRONIZED =
wenzelm@28578
     8
sig
wenzelm@28578
     9
  type 'a var
wenzelm@28578
    10
  val var: string -> 'a -> 'a var
wenzelm@28580
    11
  val value: 'a var -> 'a
wenzelm@28580
    12
  val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
wenzelm@28580
    13
  val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
wenzelm@28578
    14
  val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
wenzelm@28578
    15
  val change: 'a var -> ('a -> 'a) -> unit
wenzelm@28578
    16
end;
wenzelm@28578
    17
wenzelm@28578
    18
structure Synchronized: SYNCHRONIZED =
wenzelm@28578
    19
struct
wenzelm@28578
    20
wenzelm@28578
    21
(* state variables *)
wenzelm@28578
    22
wenzelm@28578
    23
datatype 'a var = Var of
wenzelm@28578
    24
 {name: string,
wenzelm@28578
    25
  lock: Mutex.mutex,
wenzelm@28578
    26
  cond: ConditionVar.conditionVar,
wenzelm@32738
    27
  var: 'a Unsynchronized.ref};
wenzelm@28578
    28
wenzelm@28578
    29
fun var name x = Var
wenzelm@28578
    30
 {name = name,
wenzelm@28578
    31
  lock = Mutex.mutex (),
wenzelm@28578
    32
  cond = ConditionVar.conditionVar (),
wenzelm@32738
    33
  var = Unsynchronized.ref x};
wenzelm@28578
    34
wenzelm@32592
    35
fun value (Var {var, ...}) = ! var;
wenzelm@28580
    36
wenzelm@28578
    37
wenzelm@28578
    38
(* synchronized access *)
wenzelm@28578
    39
wenzelm@28580
    40
fun timed_access (Var {name, lock, cond, var}) time_limit f =
wenzelm@28578
    41
  SimpleThread.synchronized name lock (fn () =>
wenzelm@28578
    42
    let
wenzelm@28580
    43
      fun try_change () =
wenzelm@28580
    44
        let val x = ! var in
wenzelm@28580
    45
          (case f x of
wenzelm@28580
    46
            SOME (y, x') => (var := x'; SOME y)
wenzelm@28580
    47
          | NONE =>
wenzelm@32295
    48
              (case Multithreading.sync_wait NONE (time_limit x) cond lock of
wenzelm@32295
    49
                Exn.Result true => try_change ()
wenzelm@32295
    50
              | Exn.Result false => NONE
wenzelm@32295
    51
              | Exn.Exn exn => reraise exn))
wenzelm@28580
    52
        end;
wenzelm@28580
    53
      val res = try_change ();
wenzelm@28578
    54
      val _ = ConditionVar.broadcast cond;
wenzelm@28578
    55
    in res end);
wenzelm@28578
    56
wenzelm@28580
    57
fun guarded_access var f = the (timed_access var (K NONE) f);
wenzelm@28580
    58
wenzelm@28580
    59
wenzelm@28580
    60
(* unconditional change *)
wenzelm@28580
    61
wenzelm@28580
    62
fun change_result var f = guarded_access var (SOME o f);
wenzelm@28578
    63
fun change var f = change_result var (fn x => ((), f x));
wenzelm@28578
    64
wenzelm@28578
    65
end;