src/Pure/Concurrent/synchronized.ML
author wenzelm
Thu, 22 Oct 2009 15:19:44 +0200
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;
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
    Author:     Fabian Immler and Makarius
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     3
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     4
State variables with synchronized access.
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     5
*)
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     6
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     7
signature SYNCHRONIZED =
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     8
sig
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
     9
  type 'a var
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    10
  val var: string -> 'a -> 'a var
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    11
  val value: 'a var -> 'a
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    12
  val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    13
  val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    14
  val readonly_access: 'a var -> ('a -> 'b option) -> 'b
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    15
  val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    16
  val change: 'a var -> ('a -> 'a) -> unit
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    17
  val assign: 'a var -> ('a -> 'a) -> unit
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    18
end;
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    19
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    20
structure Synchronized: SYNCHRONIZED =
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    21
struct
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    22
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    23
(* state variables *)
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    24
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    25
datatype 'a var = Var of
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    26
 {name: string,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    27
  lock: Mutex.mutex,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    28
  cond: ConditionVar.conditionVar,
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32592
diff changeset
    29
  var: 'a Unsynchronized.ref};
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    30
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    31
fun var name x = Var
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    32
 {name = name,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    33
  lock = Mutex.mutex (),
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    34
  cond = ConditionVar.conditionVar (),
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32592
diff changeset
    35
  var = Unsynchronized.ref x};
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    36
32592
e29c0b7dcf66 Synchronized.value does not require locking, since assigments are atomic;
wenzelm
parents: 32295
diff changeset
    37
fun value (Var {var, ...}) = ! var;
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    38
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    39
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    40
(* synchronized access *)
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    41
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    42
fun access {time_limit, readonly, finish} (Var {name, lock, cond, var}) f =
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    43
  SimpleThread.synchronized name lock (fn () =>
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    44
    let
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    45
      fun try_change () =
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    46
        let val x = ! var in
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    47
          (case f x of
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    48
            NONE =>
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    49
              (case Multithreading.sync_wait NONE (time_limit x) cond lock of
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    50
                Exn.Result true => try_change ()
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    51
              | Exn.Result false => NONE
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    52
              | Exn.Exn exn => reraise exn)
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    53
          | SOME (y, x') =>
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    54
              if readonly then SOME y
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    55
              else
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    56
                let
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    57
                  val _ = magic_immutability_test var
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    58
                    andalso raise Fail ("Attempt to change finished variable " ^ quote name);
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    59
                  val _ = var := x';
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    60
                  val _ = if finish then magic_immutability_mark var else ();
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    61
                in SOME y end)
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    62
        end;
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    63
      val res = try_change ();
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    64
      val _ = ConditionVar.broadcast cond;
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    65
    in res end);
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    66
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    67
fun timed_access var time_limit f =
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    68
  access {time_limit = time_limit, readonly = false, finish = false} var f;
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    69
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    70
fun guarded_access var f = the (timed_access var (K NONE) f);
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    71
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    72
fun readonly_access var f =
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    73
  the (access {time_limit = K NONE, readonly = true, finish = false} var
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    74
    (fn x => (case f x of NONE => NONE | SOME y => SOME (y, x))));
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    75
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    76
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    77
(* unconditional change *)
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    78
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    79
fun change_result var f = guarded_access var (SOME o f);
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    80
fun change var f = change_result var (fn x => ((), f x));
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    81
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    82
fun assign var f =
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    83
  the (access {time_limit = K NONE, readonly = false, finish = true} var
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    84
    (fn x => SOME ((), f x)));
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    85
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    86
end;