28578
|
1 |
(* Title: Pure/Concurrent/synchronized.ML
|
|
2 |
Author: Fabian Immler and Makarius
|
|
3 |
|
|
4 |
State variables with synchronized access.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature SYNCHRONIZED =
|
|
8 |
sig
|
|
9 |
type 'a var
|
|
10 |
val var: string -> 'a -> 'a var
|
28580
|
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
|
28578
|
14 |
val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
|
|
15 |
val change: 'a var -> ('a -> 'a) -> unit
|
|
16 |
end;
|
|
17 |
|
|
18 |
structure Synchronized: SYNCHRONIZED =
|
|
19 |
struct
|
|
20 |
|
|
21 |
(* state variables *)
|
|
22 |
|
|
23 |
datatype 'a var = Var of
|
|
24 |
{name: string,
|
|
25 |
lock: Mutex.mutex,
|
|
26 |
cond: ConditionVar.conditionVar,
|
|
27 |
var: 'a ref};
|
|
28 |
|
|
29 |
fun var name x = Var
|
|
30 |
{name = name,
|
|
31 |
lock = Mutex.mutex (),
|
|
32 |
cond = ConditionVar.conditionVar (),
|
|
33 |
var = ref x};
|
|
34 |
|
28580
|
35 |
fun value (Var {name, lock, cond, var}) = SimpleThread.synchronized name lock (fn () => ! var);
|
|
36 |
|
28578
|
37 |
|
|
38 |
(* synchronized access *)
|
|
39 |
|
28580
|
40 |
fun timed_access (Var {name, lock, cond, var}) time_limit f =
|
28578
|
41 |
SimpleThread.synchronized name lock (fn () =>
|
|
42 |
let
|
28580
|
43 |
fun try_change () =
|
|
44 |
let val x = ! var in
|
|
45 |
(case f x of
|
|
46 |
SOME (y, x') => (var := x'; SOME y)
|
|
47 |
| NONE =>
|
|
48 |
(case time_limit x of
|
|
49 |
NONE => (ConditionVar.wait (cond, lock); try_change ())
|
|
50 |
| SOME t =>
|
|
51 |
if ConditionVar.waitUntil (cond, lock, t) then try_change ()
|
|
52 |
else NONE))
|
|
53 |
end;
|
|
54 |
val res = try_change ();
|
28578
|
55 |
val _ = ConditionVar.broadcast cond;
|
|
56 |
in res end);
|
|
57 |
|
28580
|
58 |
fun guarded_access var f = the (timed_access var (K NONE) f);
|
|
59 |
|
|
60 |
|
|
61 |
(* unconditional change *)
|
|
62 |
|
|
63 |
fun change_result var f = guarded_access var (SOME o f);
|
28578
|
64 |
fun change var f = change_result var (fn x => ((), f x));
|
|
65 |
|
|
66 |
end;
|