1 open lock
 2 
 3 (* A weak reference is a pair of a strong reference [r] and a lock
 4    that protects the permission [r @ ref a]. *)
 5 
 6 (* TEMPORARY a type abbreviation would be more convenient here *)
 7 
 8 data wref a =
 9   WRef { contents: (r: unknown, lock (r @ ref a)) }
10 
11 (* Allocation. *)
12 
13 val new [a] (consumes x: a) : wref a =
14   let r = newref x in
15   let l : lock (r @ ref a) = new () in
16   WRef { contents = (r, l) }
17 
18 (* Atomic swap. *)
19 
20 val swap [a] (r: wref a, consumes y: a) : a =
21   let r, l = r.contents in
22   acquire l;
23   let x = r.contents in
24   r.contents <- y;
25   release l;
26   x
27 
28 (* Get. *)
29 
30 (* One might be tempted to believe that a critical section is not
31    needed here, since a single read (or write) instruction is atomic
32    anyway. However, removing the acquire/release instructions here
33    would be unsound (and ill-typed, of course). For instance, an
34    attempt to [get] while an [update] is in progress would be
35    dangerous. Thanks to the lock, such an attempt will block until
36    [update] is finished. *)
37 
38 val get [a] duplicable a => (r: wref a) : a =
39   let r, l = r.contents in
40   acquire l;
41   let x = r.contents in
42   release l;
43   x
44 
45 (* Set. *)
46 
47 val set [a] (r: wref a, consumes y: a) : () =
48   let r, l = r.contents in
49   acquire l;
50   r.contents <- y;
51   release l
52 
53 (* Update. *)
54 
55 val update [a, b, p : perm] (r: wref a, f: (consumes (a | p)) -> (a, b) | consumes p) : b =
56   let r, l = r.contents in
57   acquire l;
58   let x = r.contents in
59   let y, result = f x in
60   (* The test [if x != y] is not required. It may or may not save time.
61      Anyway, it is interesting that the code is well-typed in its presence.
62      In the branch where [x == y], this equality is used to transform the
63      permission [y @ a] into [x @ a]. (I think!) *)
64   if x != y then
65     r.contents <- y;
66   release l;
67   result
68 
69 val borrow [a, b, p : perm] (r: wref a, f: (a | consumes p) -> b | consumes p) : b =
70   let r, l = r.contents in
71   acquire l;
72   let x = r.contents in
73   let result = f x in
74   release l;
75   result
76 
77 (*
78 Local Variables:
79 compile-command: "../mezzo wref.mz"
80 End:
81 *)