src/Pure/Concurrent/synchronized.ML
author wenzelm
Thu, 03 Mar 2016 15:23:02 +0100
changeset 62505 9e2a65912111
parent 59195 f8588372d70e
child 62663 bea354f6ff21
permissions -rw-r--r--
clarified modules; tuned signature;
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
56685
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents: 52537
diff changeset
     4
Synchronized variables.
28578
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
56692
8219a65b24e3 synchronized access, similar to ML version;
wenzelm
parents: 56685
diff changeset
    21
(* state variable *)
28578
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
59139
e557a9ddee5f Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
wenzelm
parents: 59054
diff changeset
    36
fun value (Var {name, lock, var, ...}) =
e557a9ddee5f Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
wenzelm
parents: 59054
diff changeset
    37
  Multithreading.synchronized name lock (fn () => ! 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
35015
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    42
fun timed_access (Var {name, lock, cond, var}) time_limit f =
59054
61b723761dff load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents: 56692
diff changeset
    43
  Multithreading.synchronized name lock (fn () =>
28578
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
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43727
diff changeset
    50
                Exn.Res true => try_change ()
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43727
diff changeset
    51
              | Exn.Res false => NONE
62505
9e2a65912111 clarified modules;
wenzelm
parents: 59195
diff changeset
    52
              | Exn.Exn exn => Exn.reraise exn)
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    53
          | SOME (y, x') =>
35015
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    54
              uninterruptible (fn _ => fn () =>
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    55
                (var := x'; ConditionVar.broadcast cond; SOME y)) ())
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    56
        end;
35015
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    57
    in try_change () end);
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    58
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    59
fun guarded_access var f = the (timed_access var (K NONE) f);
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    60
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    61
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    62
(* unconditional change *)
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    63
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    64
fun change_result var f = guarded_access var (SOME o f);
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    65
fun change var f = change_result var (fn x => ((), f x));
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    66
35015
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    67
end;
33060
e66b41782cb5 support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents: 32738
diff changeset
    68
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    69
end;