equal
deleted
inserted
replaced
31 {name = name, |
31 {name = name, |
32 lock = Mutex.mutex (), |
32 lock = Mutex.mutex (), |
33 cond = ConditionVar.conditionVar (), |
33 cond = ConditionVar.conditionVar (), |
34 var = Unsynchronized.ref x}; |
34 var = Unsynchronized.ref x}; |
35 |
35 |
36 fun value (Var {var, ...}) = ! var; |
36 fun value (Var {name, lock, var, ...}) = |
|
37 Multithreading.synchronized name lock (fn () => ! var); |
37 |
38 |
38 |
39 |
39 (* synchronized access *) |
40 (* synchronized access *) |
40 |
41 |
41 fun timed_access (Var {name, lock, cond, var}) time_limit f = |
42 fun timed_access (Var {name, lock, cond, var}) time_limit f = |