Added structure to spin lock chapter. Added some clarifications and r…

…ephrased some paragraphs. Refactored to use token RA, and reordered some definitions. Fixed adequacy.

exercises/adequacy.v

@@ -1,4 +1,5 @@
 From iris.algebra Require Import excl.
+From iris.base_logic.lib Require Export token.
 From iris.heap_lang Require Import adequacy lang proofmode notation par.
 From exercises Require Import spin_lock.
 
@@ -87,15 +88,13 @@ Definition not_stuck e σ :=
 *)
 Definition progΣ := #[
   heapΣ; (* The resources required for heaplang itself *)
-  GFunctor (exclR unitO) (* The camera we used for spin-lock *)
+  tokenΣ (* The camera we used for spin-lock *)
 ].
 
 (** Finally we can combine the pieces to prove adequacy. *)
 Lemma prog_adequacy σ : adequate NotStuck prog σ (λ v _, v = #0 ∨ v = #1).
 Proof.
   apply (heap_adequacy progΣ).
   iIntros "%_ _".
-  unshelve iApply prog_spec.
-  apply (subG_inG _ (GFunctor (exclR unitO))).
-  apply subG_app_r, subG_refl.
+  iApply prog_spec.
 Qed.

exercises/spin_lock.v

@@ -1,22 +1,30 @@
 From iris.algebra Require Import excl.
-From iris.base_logic.lib Require Export invariants.
+From iris.base_logic.lib Require Export invariants token.
 From iris.heap_lang Require Import lang proofmode notation.
 
+(* ################################################################# *)
+(** * Case Study: Spin Lock *)
+
+(* ================================================================= *)
+(** ** Implementation *)
+
 (**
   A spin-lock consists of a pointer to a boolean. This boolean tells us
   whether the lock is currently locked or not.
 
-  To make a new lock, we simply allocate a new boolean.
+  To make a new lock, we simply allocate a new boolean which is
+  initially [false], signifying that the lock is unlocked.
 *)
 Definition mk_lock : val :=
   λ: <>, ref #false.
 
 (**
-  To acquire the lock, we use [CAS l false true] (compare and set).
-  This is an atomic operation that updated l to true if l was false.
-  [CAS] then evaluates to whether l was updated.
-  If the [CAS] fails, it means that the lock is currently acquired
-  somewhere else. So we simply again, until the lock is free.
+  To acquire the lock, we use [CAS l false true] (compare and set). This
+  instruction atomically writes [true] to location [l], if [l] contains
+  [false]. The [CAS] instruction then returns a boolean, signifying
+  whether [l] was updated. If the [CAS] fails, it means that the lock is
+  currently acquired somewhere else. So we simply try again, until the lock
+  is free.
 *)
 Definition acquire : val :=
   rec: "acquire" "l" :=
@@ -26,67 +34,98 @@ Definition acquire : val :=
     "acquire" "l".
 
 (**
-  To release a lock, we simply update the boolean to false. As such
+  To release a lock, we simply update the boolean to [false]. As such,
   it is only safe to call release when we are the ones who locked it.
 *)
 Definition release : val :=
   λ: "l", "l" <- #false.
 
+(* ================================================================= *)
+(** ** Representation Predicates *)
+
+(**
+  Intuitively, a lock protects resources. For instance, it can protect a
+  location in memory by allowing only one thread to access it at a time.
+  In terms of ownership, when the lock is unlocked and no thread is
+  trying to access the protected resource, then the resource is _owned
+  by the lock_. When a thread acquires the lock, ownership of the
+  protected resource is transferred to the acquiring thread. Once said
+  thread releases the lock, it must transfer the protected resources
+  back to the lock.
+
+  Therefore, our representation predicate will be parametrised by an
+  arbitrary predicate [P], which describes the resources the lock should
+  protect.
+*)
+
 Section proofs.
 Context `{heapGS Σ}.
-Let N := nroot .@ "lock".
 
 (**
   We use ghost state to describe that the lock is only ever acquired
-  once at a time. To do this we simply need ghost state that is
-  exclusive. So naturally we will use the exclusive camera. This
-  camera is generic over state, however, we don't need this feature. So
-  we will instantiate it with the unit type.
+  once at a time. The core property we are after here is exclusivity. So
+  naturally, we will use the exclusive RA. Recall that this resource
+  algebra is generic. However, we just need one exclusive element, so we
+  will instantiate the exclusive RA with the unit OFE: [exclR unitO].
+  Note that this is exactly the resource algebra we used to define
+  tokens. As such, we will reuse tokens here, but rename them to clarify
+  their intent.
 *)
-Context `{!inG Σ (exclR unitO)}.
+Context `{!tokenG Σ}.
 
 (**
-  We will think of the name of our ghost state as the name of the
-  lock. Its invariant will be that l maps to a boolean b, and if
-  b is false, meaning the lock is unlocked, then the invariant owns
-  both the resource and the critical area protected by the lock.
+  The knowledge that we have acquired the lock is then represented by
+  ownership of the token.
 *)
-Definition lock_inv γ l P : iProp Σ :=
-  ∃ b : bool, l ↦ #b ∗
-  if b then True
-  else own γ (Excl ()) ∗ P.
+Definition locked γ : iProp Σ := token γ.
 
-Definition is_lock γ v P : iProp Σ :=
-  ∃ l : loc, ⌜v = #l⌝ ∗ inv N (lock_inv γ l P).
+(**
+  Allocation and exclusivity of the [locked] predicate then follows
+  directly from the properties of the token.
+*)
+Lemma locked_alloc : ⊢ |==> ∃ γ, locked γ.
+Proof. apply token_alloc. Qed.
+
+Lemma locked_excl γ : locked γ -∗ locked γ -∗ False.
+Proof. apply token_exclusive. Qed.
 
 (**
-  The knowledge that we have acquired is then represented by
-  ownership of the resource.
+  We will need our representation predicate for the lock, [is_lock], to
+  be persistent so that it can be shared among participating threads.
+  Therefore, we will be needing an invariant. The invariant states that
+  the location representing the lock, [l], maps to a boolean [b], and if
+  [b] is [false], meaning the lock is unlocked, then the invariant owns
+  both the protected resources and the [locked] predicate.
 *)
-Definition locked γ : iProp Σ := own γ (Excl ()).
+Let N := nroot .@ "lock".
+
+Definition lock_inv γ l P : iProp Σ :=
+  ∃ b : bool, l ↦ #b ∗
+  if b then True
+  else locked γ ∗ P.
 
 (**
-  We need the ghost state to prove that this is exclusive.
+  The representation predicate then just asserts that the value
+  representing the lock is a location which satisfies the lock
+  invariant.
 *)
-Lemma locked_excl γ : locked γ -∗ locked γ -∗ False.
-Proof.
-  iIntros "H1 H2".
-  iPoseProof (own_valid_2 with "H1 H2") as "%H".
-  cbv in H.
-  done.
-Qed.
+Definition is_lock γ v P : iProp Σ :=
+  ∃ l : loc, ⌜v = #l⌝ ∗ inv N (lock_inv γ l P).
+
+(* ================================================================= *)
+(** ** Specifications *)
 
 (**
-  Making a new lock consists of giving away ownership of the critical
-  area to the lock.
+  Making a new lock consists of giving away ownership of the resources
+  to be protected, [P], to the lock.
 *)
-Lemma mk_lock_spec P : {{{ P }}} mk_lock #() {{{ γ v, RET v; is_lock γ v P }}}.
+Lemma mk_lock_spec P :
+  {{{ P }}} mk_lock #() {{{ γ v, RET v; is_lock γ v P }}}.
 Proof.
   iIntros "%Φ HP HΦ".
   wp_lam.
   wp_alloc l as "Hl".
-  iMod (own_alloc (Excl ())) as "[%γ Hγ]".
-  { done. }
+  iMod locked_alloc as "[%γ Hγ]".
   iMod (inv_alloc N _ (lock_inv γ l P) with "[HP Hl Hγ]") as "I".
   {
     iNext.
@@ -100,10 +139,11 @@ Proof.
 Qed.
 
 (**
-  Acquiring the lock should result in access to the critical area,
-  as well as knowledge that the lock has been locked.
+  Acquiring the lock should grant access to the protected resources, as
+  well as knowledge that the lock has been locked.
 *)
-Lemma acquire_spec γ v P : {{{ is_lock γ v P }}} acquire v {{{ RET #(); locked γ ∗ P }}}.
+Lemma acquire_spec γ v P :
+  {{{ is_lock γ v P }}} acquire v {{{ RET #(); locked γ ∗ P }}}.
 Proof.
   iIntros "%Φ (%l & -> & #I) HΦ".
   iLöb as "IH".
@@ -133,20 +173,20 @@ Proof.
     iApply ("HΦ" with "Hγ").
 Qed.
 
-Lemma release_spec γ v P : {{{ is_lock γ v P ∗ locked γ ∗ P }}} release v {{{ RET #(); True }}}.
+(**
+  Releasing the lock consists of transferring back the protected
+  resources and the [locked] predicate to the lock.
+*)
+Lemma release_spec γ v P :
+  {{{ is_lock γ v P ∗ locked γ ∗ P }}} release v {{{ RET #(); True }}}.
 Proof.
-  iIntros "%Φ ((%l & -> & I) & Hγ & HP) HΦ".
-  wp_lam.
-  iInv "I" as "(%b & Hl & _)".
-  wp_store.
-  iModIntro.
-  iSplitL "Hγ Hl HP".
-  - iNext.
-    iExists false.
-    iFrame.
-  - by iApply "HΦ".
-Qed.
+  (* exercise *)
+Admitted.
+
+(* ================================================================= *)
+(** ** Example Client *)
 
+(** Consider the following client of lock. *)
 Definition prog : expr :=
   let: "x" := ref #0 in
   let: "l" := mk_lock #() in
@@ -160,14 +200,19 @@ Definition prog : expr :=
   !"x".
 
 (**
-  x can take on the values of 0, 1, and 7. However, we should not
-  observe 7, as it is overridden before the lock is released.
+  [x] can take on the values of [0], [1], and [7]. However, we should
+  not observe [7], as it is overridden before the lock is released.
 *)
 Lemma prog_spec : ⊢ WP prog {{ v, ⌜v = #0 ∨ v = #1⌝}}.
 Proof.
   rewrite /prog.
   wp_alloc x as "Hx".
   wp_pures.
+  (**
+    For this program, the resource to be protected is the points-to
+    predicate for [x], but where the value pointed to by [x] can be only
+    [0] or [1].
+  *)
   wp_apply (mk_lock_spec (∃ v, x ↦ v ∗ ⌜v = #0 ∨ v = #1⌝) with "[Hx]").
   {
     iExists #0.

theories/adequacy.v

@@ -1,4 +1,5 @@
 From iris.algebra Require Import excl.
+From iris.base_logic.lib Require Export token.
 From iris.heap_lang Require Import adequacy lang proofmode notation par.
 From solutions Require Import spin_lock.
 
@@ -87,15 +88,13 @@ Definition not_stuck e σ :=
 *)
 Definition progΣ := #[
   heapΣ; (* The resources required for heaplang itself *)
-  GFunctor (exclR unitO) (* The camera we used for spin-lock *)
+  tokenΣ (* The camera we used for spin-lock *)
 ].
 
 (** Finally we can combine the pieces to prove adequacy. *)
 Lemma prog_adequacy σ : adequate NotStuck prog σ (λ v _, v = #0 ∨ v = #1).
 Proof.
   apply (heap_adequacy progΣ).
   iIntros "%_ _".
-  unshelve iApply prog_spec.
-  apply (subG_inG _ (GFunctor (exclR unitO))).
-  apply subG_app_r, subG_refl.
+  iApply prog_spec.
 Qed.