1 (* A weak reference is a duplicable mutable container, whose content 2 type is fixed at creation time (i.e., it does not allow strong 3 updates). In other words, it is an ML reference. *) 4 5 (* Because a weak reference is duplicable, multiple threads may 6 simultaneously attempt to access (read or write) the reference. 7 Technically, this does not constitute a race condition, because 8 a lock is used internally to protect the reference. *) 9 10 abstract wref a 11 fact duplicable (wref a) 12 13 (* Allocation. *) 14 15 val new: [a] (consumes a) -> wref a 16 17 (* Atomic swap. *) 18 19 val swap: [a] (wref a, consumes a) -> a 20 21 (* Get. *) 22 23 val get: [a] duplicable a => wref a -> a 24 25 (* Set. *) 26 27 val set: [a] (wref a, consumes a) -> () 28 29 (* [update] can be viewed as a version of [swap] where the new value 30 is computed in terms of the previous value. The lock remains taken 31 while the computation is in progress, so [update] must be used with 32 care. *) 33 34 val update: [a, b, p : perm] ( 35 r: wref a, 36 f: (consumes (a | p)) -> (a, b) 37 | consumes p) -> b 38 39 (* [borrow] can be viewed as a degenerate version of [update] where 40 the function [f] temporarily has access to the content of the 41 reference [r], but cannot modify it. *) 42 43 val borrow: [a, b, p : perm] ( 44 r: wref a, 45 f: (a | consumes p) -> b 46 | consumes p) -> b