src/Pure/Concurrent/synchronized.ML
author wenzelm
Sat Aug 01 00:09:45 2009 +0200 (2009-08-01)
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;
wenzelm@28578
     1
(*  Title:      Pure/Concurrent/synchronized.ML
wenzelm@28578
     2
    Author:     Fabian Immler and Makarius
wenzelm@28578
     3
wenzelm@28578
     4
State variables with synchronized access.
wenzelm@28578
     5
*)
wenzelm@28578
     6
wenzelm@28578
     7
signature SYNCHRONIZED =
wenzelm@28578
     8
sig
wenzelm@28578
     9
  type 'a var
wenzelm@28578
    10
  val var: string -> 'a -> 'a var
wenzelm@32252
    11
  val peek: 'a var -> 'a
wenzelm@28580
    12
  val value: 'a var -> 'a
wenzelm@28580
    13
  val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
wenzelm@28580
    14
  val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
wenzelm@28578
    15
  val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
wenzelm@28578
    16
  val change: 'a var -> ('a -> 'a) -> unit
wenzelm@28578
    17
end;
wenzelm@28578
    18
wenzelm@28578
    19
structure Synchronized: SYNCHRONIZED =
wenzelm@28578
    20
struct
wenzelm@28578
    21
wenzelm@28578
    22
(* state variables *)
wenzelm@28578
    23
wenzelm@28578
    24
datatype 'a var = Var of
wenzelm@28578
    25
 {name: string,
wenzelm@28578
    26
  lock: Mutex.mutex,
wenzelm@28578
    27
  cond: ConditionVar.conditionVar,
wenzelm@28578
    28
  var: 'a ref};
wenzelm@28578
    29
wenzelm@28578
    30
fun var name x = Var
wenzelm@28578
    31
 {name = name,
wenzelm@28578
    32
  lock = Mutex.mutex (),
wenzelm@28578
    33
  cond = ConditionVar.conditionVar (),
wenzelm@28578
    34
  var = ref x};
wenzelm@28578
    35
wenzelm@32252
    36
fun peek (Var {var, ...}) = ! var;  (*unsynchronized!*)
wenzelm@32252
    37
wenzelm@28580
    38
fun value (Var {name, lock, cond, var}) = SimpleThread.synchronized name lock (fn () => ! var);
wenzelm@28580
    39
wenzelm@28578
    40
wenzelm@28578
    41
(* synchronized access *)
wenzelm@28578
    42
wenzelm@28580
    43
fun timed_access (Var {name, lock, cond, var}) time_limit f =
wenzelm@28578
    44
  SimpleThread.synchronized name lock (fn () =>
wenzelm@28578
    45
    let
wenzelm@28580
    46
      fun try_change () =
wenzelm@28580
    47
        let val x = ! var in
wenzelm@28580
    48
          (case f x of
wenzelm@28580
    49
            SOME (y, x') => (var := x'; SOME y)
wenzelm@28580
    50
          | NONE =>
wenzelm@32295
    51
              (case Multithreading.sync_wait NONE (time_limit x) cond lock of
wenzelm@32295
    52
                Exn.Result true => try_change ()
wenzelm@32295
    53
              | Exn.Result false => NONE
wenzelm@32295
    54
              | Exn.Exn exn => reraise exn))
wenzelm@28580
    55
        end;
wenzelm@28580
    56
      val res = try_change ();
wenzelm@28578
    57
      val _ = ConditionVar.broadcast cond;
wenzelm@28578
    58
    in res end);
wenzelm@28578
    59
wenzelm@28580
    60
fun guarded_access var f = the (timed_access var (K NONE) f);
wenzelm@28580
    61
wenzelm@28580
    62
wenzelm@28580
    63
(* unconditional change *)
wenzelm@28580
    64
wenzelm@28580
    65
fun change_result var f = guarded_access var (SOME o f);
wenzelm@28578
    66
fun change var f = change_result var (fn x => ((), f x));
wenzelm@28578
    67
wenzelm@28578
    68
end;