1 (* A lock protects a permission [p], which usually is not duplicable.
 2    The lock itself is duplicable, so multiple threads may simultaneously
 3    attempt to acquire it. *)
 4 
 5 abstract lock (p: perm)
 6 fact duplicable (lock p)
 7 
 8 (* The permission [held l], where [l] is a lock, is a witness that the
 9    lock [l] is held. This permission is not duplicable. This allows
10    the type system to prevent calling [release l] unless the lock [l]
11    is held. *)
12 
13 abstract held (l: term): perm
14 
15 (* Creation. *)
16 
17 (* The invariant [p] is fixed at creation time. *)
18 
19 (* When the lock is created, it is available; for this reason, [new]
20    consumes the permission [p]. One could offer a variant of [new]
21    where the lock is initially held; this variant would not require
22    [p], and would produce [held l]. *)
23 
24 val new: [p: perm] (| consumes p) -> lock p
25 
26 (* Acquisition. *)
27 
28 val acquire:     [p: perm] (l: lock p) -> (| p * held l)
29 val try_acquire: [p: perm] (l: lock p) -> rich_bool empty (p * held l)
30 
31 (* Release. *)
32 
33 val release: [p: perm] (l: lock p | consumes (p * held l)) -> ()
34 
35 (* A well-balanced acquire/release pair. *)
36 
37 val borrow: [p: perm, q: perm, b] (
38   l: lock p,
39   f: (| p * consumes q) -> b
40 | consumes q
41 ) -> b
42