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