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