author | wenzelm |
Tue, 29 Sep 2009 11:49:22 +0200 | |
changeset 32738 | 15bb09ca0378 |
parent 32592 | e29c0b7dcf66 |
child 33060 | e66b41782cb5 |
permissions | -rw-r--r-- |
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, |
|
32738 | 27 |
var: 'a Unsynchronized.ref}; |
28578 | 28 |
|
29 |
fun var name x = Var |
|
30 |
{name = name, |
|
31 |
lock = Mutex.mutex (), |
|
32 |
cond = ConditionVar.conditionVar (), |
|
32738 | 33 |
var = Unsynchronized.ref x}; |
28578 | 34 |
|
32592
e29c0b7dcf66
Synchronized.value does not require locking, since assigments are atomic;
wenzelm
parents:
32295
diff
changeset
|
35 |
fun value (Var {var, ...}) = ! var; |
28580 | 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 => |
|
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
48 |
(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
|
49 |
Exn.Result true => try_change () |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
50 |
| Exn.Result false => NONE |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
51 |
| Exn.Exn exn => reraise exn)) |
28580 | 52 |
end; |
53 |
val res = try_change (); |
|
28578 | 54 |
val _ = ConditionVar.broadcast cond; |
55 |
in res end); |
|
56 |
||
28580 | 57 |
fun guarded_access var f = the (timed_access var (K NONE) f); |
58 |
||
59 |
||
60 |
(* unconditional change *) |
|
61 |
||
62 |
fun change_result var f = guarded_access var (SOME o f); |
|
28578 | 63 |
fun change var f = change_result var (fn x => ((), f x)); |
64 |
||
65 |
end; |