src/Pure/Concurrent/synchronized.ML
author wenzelm
Fri, 05 Jul 2013 15:38:03 +0200
changeset 52530 99dd8b4ef3fe
parent 43761 e72ba84ae58f
child 52537 4b5941730bd8
permissions -rw-r--r--
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
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
40449
9c390868d255 added general Synchronized.counter convenience;
wenzelm
parents: 37216
diff changeset
    16
  val counter: unit -> unit -> int
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    17
end;
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    18
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    19
structure Synchronized: SYNCHRONIZED =
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    20
struct
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    21
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    22
(* state variables *)
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    23
35015
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    24
abstype 'a var = Var of
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    25
 {name: string,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    26
  lock: Mutex.mutex,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    27
  cond: ConditionVar.conditionVar,
35015
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    28
  var: 'a Unsynchronized.ref}
efafb3337ef3 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents: 33060
diff changeset
    29
with
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
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 =
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 35015
diff changeset
    43
  Simple_Thread.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
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') =>
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
40449
9c390868d255 added general Synchronized.counter convenience;
wenzelm
parents: 37216
diff changeset
    69
9c390868d255 added general Synchronized.counter convenience;
wenzelm
parents: 37216
diff changeset
    70
(* unique identifiers > 0 *)
9c390868d255 added general Synchronized.counter convenience;
wenzelm
parents: 37216
diff changeset
    71
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 43761
diff changeset
    72
(*NB: ML ticks forwards, JVM ticks backwards*)
40449
9c390868d255 added general Synchronized.counter convenience;
wenzelm
parents: 37216
diff changeset
    73
fun counter () =
9c390868d255 added general Synchronized.counter convenience;
wenzelm
parents: 37216
diff changeset
    74
  let
43727
a0c3de0573d4 made SML/NJ happy;
wenzelm
parents: 40449
diff changeset
    75
    val counter = var "counter" (0: int);
40449
9c390868d255 added general Synchronized.counter convenience;
wenzelm
parents: 37216
diff changeset
    76
    fun next () =
9c390868d255 added general Synchronized.counter convenience;
wenzelm
parents: 37216
diff changeset
    77
      change_result counter
9c390868d255 added general Synchronized.counter convenience;
wenzelm
parents: 37216
diff changeset
    78
        (fn i =>
43727
a0c3de0573d4 made SML/NJ happy;
wenzelm
parents: 40449
diff changeset
    79
          let val j = i + (1: int)
40449
9c390868d255 added general Synchronized.counter convenience;
wenzelm
parents: 37216
diff changeset
    80
          in (j, j) end);
9c390868d255 added general Synchronized.counter convenience;
wenzelm
parents: 37216
diff changeset
    81
  in next end;
9c390868d255 added general Synchronized.counter convenience;
wenzelm
parents: 37216
diff changeset
    82
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    83
end;