author | wenzelm |
Tue, 14 Mar 2017 19:46:53 +0100 | |
changeset 65236 | 4fa82bbb394e |
parent 64276 | 622f4e4ac388 |
child 68597 | afa7c5a239e6 |
permissions | -rw-r--r-- |
28578 | 1 |
(* Title: Pure/Concurrent/synchronized.ML |
2 |
Author: Fabian Immler and Makarius |
|
3 |
||
56685 | 4 |
Synchronized variables. |
28578 | 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 |
||
56692 | 21 |
(* state variable *) |
28578 | 22 |
|
35015
efafb3337ef3
removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents:
33060
diff
changeset
|
23 |
abstype 'a var = Var of |
28578 | 24 |
{name: string, |
25 |
lock: Mutex.mutex, |
|
26 |
cond: ConditionVar.conditionVar, |
|
35015
efafb3337ef3
removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents:
33060
diff
changeset
|
27 |
var: 'a Unsynchronized.ref} |
efafb3337ef3
removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
wenzelm
parents:
33060
diff
changeset
|
28 |
with |
28578 | 29 |
|
30 |
fun var name x = Var |
|
31 |
{name = name, |
|
32 |
lock = Mutex.mutex (), |
|
33 |
cond = ConditionVar.conditionVar (), |
|
32738 | 34 |
var = Unsynchronized.ref x}; |
28578 | 35 |
|
59139
e557a9ddee5f
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
wenzelm
parents:
59054
diff
changeset
|
36 |
fun value (Var {name, lock, var, ...}) = |
e557a9ddee5f
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
wenzelm
parents:
59054
diff
changeset
|
37 |
Multithreading.synchronized name lock (fn () => ! var); |
28580 | 38 |
|
28578 | 39 |
|
40 |
(* synchronized access *) |
|
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 = |
59054
61b723761dff
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents:
56692
diff
changeset
|
43 |
Multithreading.synchronized name lock (fn () => |
28578 | 44 |
let |
28580 | 45 |
fun try_change () = |
46 |
let val x = ! var in |
|
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 => |
64276 | 49 |
(case Multithreading.sync_wait (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 |
62505 | 52 |
| Exn.Exn exn => Exn.reraise exn) |
33060
e66b41782cb5
support single-assigment variables -- based on magic RTS operations by David Matthews;
wenzelm
parents:
32738
diff
changeset
|
53 |
| SOME (y, x') => |
62923 | 54 |
Thread_Attributes.uninterruptible (fn _ => fn () => |
35015
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 | 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 |
|
62918 | 59 |
fun guarded_access var f = the (timed_access var (fn _ => NONE) f); |
28580 | 60 |
|
61 |
||
62 |
(* unconditional change *) |
|
63 |
||
64 |
fun change_result var f = guarded_access var (SOME o f); |
|
28578 | 65 |
fun change var f = change_result var (fn x => ((), f x)); |
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 |
|
28578 | 69 |
end; |