src/Pure/Concurrent/synchronized.ML
author wenzelm
Thu Oct 22 15:19:44 2009 +0200 (2009-10-22)
changeset 33060 e66b41782cb5
parent 32738 15bb09ca0378
child 35015 efafb3337ef3
permissions -rw-r--r--
support single-assigment variables -- based on magic RTS operations by David Matthews;
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@33060
    14
  val readonly_access: 'a var -> ('a -> 'b 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@33060
    17
  val assign: 'a var -> ('a -> 'a) -> unit
wenzelm@28578
    18
end;
wenzelm@28578
    19
wenzelm@28578
    20
structure Synchronized: SYNCHRONIZED =
wenzelm@28578
    21
struct
wenzelm@28578
    22
wenzelm@28578
    23
(* state variables *)
wenzelm@28578
    24
wenzelm@28578
    25
datatype 'a var = Var of
wenzelm@28578
    26
 {name: string,
wenzelm@28578
    27
  lock: Mutex.mutex,
wenzelm@28578
    28
  cond: ConditionVar.conditionVar,
wenzelm@32738
    29
  var: 'a Unsynchronized.ref};
wenzelm@28578
    30
wenzelm@28578
    31
fun var name x = Var
wenzelm@28578
    32
 {name = name,
wenzelm@28578
    33
  lock = Mutex.mutex (),
wenzelm@28578
    34
  cond = ConditionVar.conditionVar (),
wenzelm@32738
    35
  var = Unsynchronized.ref x};
wenzelm@28578
    36
wenzelm@32592
    37
fun value (Var {var, ...}) = ! var;
wenzelm@28580
    38
wenzelm@28578
    39
wenzelm@28578
    40
(* synchronized access *)
wenzelm@28578
    41
wenzelm@33060
    42
fun access {time_limit, readonly, finish} (Var {name, lock, cond, var}) f =
wenzelm@28578
    43
  SimpleThread.synchronized name lock (fn () =>
wenzelm@28578
    44
    let
wenzelm@28580
    45
      fun try_change () =
wenzelm@28580
    46
        let val x = ! var in
wenzelm@28580
    47
          (case f x of
wenzelm@33060
    48
            NONE =>
wenzelm@32295
    49
              (case Multithreading.sync_wait NONE (time_limit x) cond lock of
wenzelm@32295
    50
                Exn.Result true => try_change ()
wenzelm@32295
    51
              | Exn.Result false => NONE
wenzelm@33060
    52
              | Exn.Exn exn => reraise exn)
wenzelm@33060
    53
          | SOME (y, x') =>
wenzelm@33060
    54
              if readonly then SOME y
wenzelm@33060
    55
              else
wenzelm@33060
    56
                let
wenzelm@33060
    57
                  val _ = magic_immutability_test var
wenzelm@33060
    58
                    andalso raise Fail ("Attempt to change finished variable " ^ quote name);
wenzelm@33060
    59
                  val _ = var := x';
wenzelm@33060
    60
                  val _ = if finish then magic_immutability_mark var else ();
wenzelm@33060
    61
                in SOME y end)
wenzelm@28580
    62
        end;
wenzelm@28580
    63
      val res = try_change ();
wenzelm@28578
    64
      val _ = ConditionVar.broadcast cond;
wenzelm@28578
    65
    in res end);
wenzelm@28578
    66
wenzelm@33060
    67
fun timed_access var time_limit f =
wenzelm@33060
    68
  access {time_limit = time_limit, readonly = false, finish = false} var f;
wenzelm@33060
    69
wenzelm@28580
    70
fun guarded_access var f = the (timed_access var (K NONE) f);
wenzelm@28580
    71
wenzelm@33060
    72
fun readonly_access var f =
wenzelm@33060
    73
  the (access {time_limit = K NONE, readonly = true, finish = false} var
wenzelm@33060
    74
    (fn x => (case f x of NONE => NONE | SOME y => SOME (y, x))));
wenzelm@33060
    75
wenzelm@28580
    76
wenzelm@28580
    77
(* unconditional change *)
wenzelm@28580
    78
wenzelm@28580
    79
fun change_result var f = guarded_access var (SOME o f);
wenzelm@28578
    80
fun change var f = change_result var (fn x => ((), f x));
wenzelm@28578
    81
wenzelm@33060
    82
fun assign var f =
wenzelm@33060
    83
  the (access {time_limit = K NONE, readonly = false, finish = true} var
wenzelm@33060
    84
    (fn x => SOME ((), f x)));
wenzelm@33060
    85
wenzelm@28578
    86
end;