src/Pure/Concurrent/synchronized.ML
author hoelzl
Wed, 02 Apr 2014 18:35:01 +0200
changeset 56369 2704ca85be98
parent 52537 4b5941730bd8
child 56685 535d59d4ed12
permissions -rw-r--r--
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
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
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    14
  val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    15
  val change: 'a var -> ('a -> 'a) -> unit
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    16
end;
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    17
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    18
structure Synchronized: SYNCHRONIZED =
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    19
struct
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    20
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    21
(* state variables *)
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    22
35015
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    23
abstype 'a var = Var of
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    24
 {name: string,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    25
  lock: Mutex.mutex,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    26
  cond: ConditionVar.conditionVar,
35015
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    27
  var: 'a Unsynchronized.ref}
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    28
with
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    29
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    30
fun var name x = Var
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    31
 {name = name,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    32
  lock = Mutex.mutex (),
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    33
  cond = ConditionVar.conditionVar (),
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32592
diff changeset
    34
  var = Unsynchronized.ref x};
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    35
32592
e29c0b7dcf66 Synchronized.value does not require locking, since assigments are atomic;
wenzelm
parents: 32295
diff changeset
    36
fun value (Var {var, ...}) = ! var;
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    37
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    38
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    39
(* synchronized access *)
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    40
35015
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    41
fun timed_access (Var {name, lock, cond, var}) time_limit f =
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 35015
diff changeset
    42
  Simple_Thread.synchronized name lock (fn () =>
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    43
    let
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    44
      fun try_change () =
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    45
        let val x = ! var in
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    46
          (case f x of
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    47
            NONE =>
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    48
              (case Multithreading.sync_wait NONE (time_limit x) cond lock of
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43727
diff changeset
    49
                Exn.Res true => try_change ()
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43727
diff changeset
    50
              | Exn.Res false => NONE
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    51
              | Exn.Exn exn => reraise exn)
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    52
          | SOME (y, x') =>
35015
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    53
              uninterruptible (fn _ => fn () =>
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    54
                (var := x'; ConditionVar.broadcast cond; SOME y)) ())
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    55
        end;
35015
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    56
    in try_change () end);
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    57
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    58
fun guarded_access var f = the (timed_access var (K NONE) f);
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    59
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    60
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    61
(* unconditional change *)
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    62
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    63
fun change_result var f = guarded_access var (SOME o f);
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    64
fun change var f = change_result var (fn x => ((), f x));
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    65
35015
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    66
end;
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    67
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    68
end;