src/Pure/Concurrent/synchronized.ML
author wenzelm
Sat, 01 Aug 2009 00:09:45 +0200
changeset 32295 400cc493d466
parent 32286 1fb5db48002d
child 32592 e29c0b7dcf66
permissions -rw-r--r--
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts; renamed Multithreading.restricted_interrupts to Multithreading.private_interrupts; added Multithreading.sync_interrupts; Multithreading.sync_wait: more careful treatment of attributes; Multithreading.tracing: uninterruptible; Multithreading.system_out: signal within critical region, more careful sync_wait; eliminated redundant Thread.testInterrupt; Future.wait_timeout: uniform Multithreading.sync_wait; future scheduler: interruptible body (sync!), to improve reactivity; future_job: reject duplicate assignments -- system error; misc tuning;
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
32252
fd5e4a1a4ea6 added unsynchronized Synchronized.peek;
wenzelm
parents: 29564
diff changeset
    11
  val peek: 'a var -> 'a
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    12
  val value: 'a var -> 'a
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    13
  val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    14
  val guarded_access: 'a var -> ('a -> ('b * 'a) 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
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
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    24
datatype 'a var = Var of
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,
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    28
  var: 'a ref};
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 (),
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    34
  var = ref x};
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    35
32252
fd5e4a1a4ea6 added unsynchronized Synchronized.peek;
wenzelm
parents: 29564
diff changeset
    36
fun peek (Var {var, ...}) = ! var;  (*unsynchronized!*)
fd5e4a1a4ea6 added unsynchronized Synchronized.peek;
wenzelm
parents: 29564
diff changeset
    37
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    38
fun value (Var {name, lock, cond, var}) = SimpleThread.synchronized name lock (fn () => ! var);
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    39
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    40
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    41
(* synchronized access *)
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    42
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    43
fun timed_access (Var {name, lock, cond, var}) time_limit f =
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    44
  SimpleThread.synchronized name lock (fn () =>
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    45
    let
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    46
      fun try_change () =
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    47
        let val x = ! var in
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    48
          (case f x of
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    49
            SOME (y, x') => (var := x'; SOME y)
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    50
          | NONE =>
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    51
              (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
    52
                Exn.Result true => try_change ()
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    53
              | Exn.Result false => NONE
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    54
              | Exn.Exn exn => reraise exn))
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    55
        end;
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    56
      val res = try_change ();
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    57
      val _ = ConditionVar.broadcast cond;
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    58
    in res end);
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    59
28580
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    60
fun guarded_access var f = the (timed_access var (K NONE) f);
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    61
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    62
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    63
(* unconditional change *)
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    64
3f37ae257506 added value;
wenzelm
parents: 28578
diff changeset
    65
fun change_result var f = guarded_access var (SOME o f);
28578
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    66
fun change var f = change_result var (fn x => ((), f x));
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    67
c7f2a0899679 State variables with synchronized access.
wenzelm
parents:
diff changeset
    68
end;