1(*  Title:      Pure/Concurrent/synchronized.ML
2    Author:     Fabian Immler and Makarius
3
4Synchronized variables.
5*)
6
7signature SYNCHRONIZED =
8sig
9  type 'a var
10  val var: string -> 'a -> 'a var
11  val value: 'a var -> 'a
12  val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
13  val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
14  val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
15  val change: 'a var -> ('a -> 'a) -> unit
16end;
17
18structure Synchronized: SYNCHRONIZED =
19struct
20
21(* state variable *)
22
23abstype 'a var = Var of
24 {name: string,
25  lock: Mutex.mutex,
26  cond: ConditionVar.conditionVar,
27  var: 'a Unsynchronized.ref}
28with
29
30fun var name x = Var
31 {name = name,
32  lock = Mutex.mutex (),
33  cond = ConditionVar.conditionVar (),
34  var = Unsynchronized.ref x};
35
36fun value (Var {name, lock, var, ...}) =
37  Multithreading.synchronized name lock (fn () => ! var);
38
39
40(* synchronized access *)
41
42fun timed_access (Var {name, lock, cond, var}) time_limit f =
43  Multithreading.synchronized name lock (fn () =>
44    let
45      fun try_change () =
46        let val x = ! var in
47          (case f x of
48            NONE =>
49              (case Multithreading.sync_wait (time_limit x) cond lock of
50                Exn.Res true => try_change ()
51              | Exn.Res false => NONE
52              | Exn.Exn exn => Exn.reraise exn)
53          | SOME (y, x') =>
54              Thread_Attributes.uninterruptible (fn _ => fn () =>
55                (var := x'; ConditionVar.broadcast cond; SOME y)) ())
56        end;
57    in try_change () end);
58
59fun guarded_access var f = valOf (timed_access var (fn _ => NONE) f);
60
61
62(* unconditional change *)
63
64fun change_result var f = guarded_access var (SOME o f);
65fun change var f = change_result var (fn x => ((), f x));
66
67end;
68
69end;
70