Remove CAS loop in release of ticket_lock.

heap_lang/lib/ticket_lock.v

 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.program_logic Require Import auth.
 From iris.proofmode Require Import invariants.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import gset.
+From iris.algebra Require Import auth gset.
 From iris.heap_lang.lib Require Export lock.
 Import uPred.
 
@@ -23,53 +22,44 @@ Definition acquire : val :=
       then wait_loop "n" "lock"
       else "acquire" "lock".
 
-Definition release : val :=
-  rec: "release" "lock" :=
-    let: "o" := !(Fst "lock") in
-    if: CAS (Fst "lock") "o" ("o" + #1)
-      then #()
-      else "release" "lock".
+Definition release : val := λ: "lock",
+  (Fst "lock") <- !(Fst "lock") + #1.
 
 Global Opaque newlock acquire release wait_loop.
 
 (** The CMRAs we need. *)
-Class tlockG Σ := TlockG {
-   tlock_G :> authG Σ (gset_disjUR nat);
-   tlock_exclG  :> inG Σ (exclR unitC)
-}.
+Class tlockG Σ :=
+  tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))).
 Definition tlockΣ : gFunctors :=
-  #[authΣ (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
+  #[ GFunctor (constRF (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat)))) ].
 
 Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
-Proof. intros [? [?%subG_inG _]%subG_inv]%subG_inv. split; apply _. Qed.
+Proof. by intros ?%subG_inG. Qed.
 
 Section proof.
   Context `{!heapG Σ, !tlockG Σ} (N : namespace).
 
-  Definition tickets_inv (n: nat) (gs: gset_disjUR nat) : iProp Σ :=
-    (gs = GSet (seq_set 0 n))%I.
-
-  Definition lock_inv (γ1 γ2: gname) (lo ln: loc) (R : iProp Σ) : iProp Σ :=
-    (∃ (o n: nat),
+  Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
+    (∃ o n : nat,
       lo ↦ #o ★ ln ↦ #n ★
-       auth_inv γ1 (tickets_inv n) ★
-       ((own γ2 (Excl ()) ★ R) ∨ auth_own γ1 (GSet {[ o ]})))%I.
+      own γ (● (Excl' o, GSet (seq_set 0 n))) ★
+      ((own γ (◯ (Excl' o, ∅)) ★ R) ∨ own γ (◯ (∅, GSet {[ o ]}))))%I.
 
-  Definition is_lock (γs: gname * gname) (l: val) (R: iProp Σ) : iProp Σ :=
-    (∃ (lo ln: loc),
+  Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
+    (∃ lo ln : loc,
        heapN ⊥ N ∧ heap_ctx ∧
-       l = (#lo, #ln)%V ∧ inv N (lock_inv (fst γs) (snd γs) lo ln R))%I.
+       lk = (#lo, #ln)%V ∧ inv N (lock_inv γ lo ln R))%I.
 
-  Definition issued (γs: gname * gname) (l : val) (x: nat) (R : iProp Σ) : iProp Σ :=
-    (∃ (lo ln: loc),
+  Definition issued (γ : gname) (lk : val) (x : nat) (R : iProp Σ) : iProp Σ :=
+    (∃ lo ln: loc,
        heapN ⊥ N ∧ heap_ctx ∧
-       l = (#lo, #ln)%V ∧ inv N (lock_inv (fst γs) (snd γs) lo ln R) ∧
-       auth_own (fst γs) (GSet {[ x ]}))%I.
+       lk = (#lo, #ln)%V ∧ inv N (lock_inv γ lo ln R) ∧
+       own γ (◯ (∅, GSet {[ x ]})))%I.
 
-  Definition locked (γs: gname * gname) : iProp Σ := own (snd γs) (Excl ())%I.
+  Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, ∅)))%I.
 
-  Global Instance lock_inv_ne n γ1 γ2 lo ln :
-    Proper (dist n ==> dist n) (lock_inv γ1 γ2 lo ln).
+  Global Instance lock_inv_ne n γs lo ln :
+    Proper (dist n ==> dist n) (lock_inv γs lo ln).
   Proof. solve_proper. Qed.
   Global Instance is_lock_ne γs n l : Proper (dist n ==> dist n) (is_lock γs l).
   Proof. solve_proper. Qed.
@@ -78,47 +68,41 @@ Section proof.
   Global Instance locked_timeless γs : TimelessP (locked γs).
   Proof. apply _. Qed.
 
-  Lemma locked_exclusive (γs: gname * gname) : (locked γs ★ locked γs ⊢ False)%I.
-  Proof. rewrite /locked -own_op own_valid. by iIntros (?). Qed.
+  Lemma locked_exclusive (γ : gname) : (locked γ ★ locked γ ⊢ False)%I.
+  Proof.
+    iIntros "[H1 H2]". iDestruct "H1" as (o1) "H1". iDestruct "H2" as (o2) "H2".
+    iCombine "H1" "H2" as "H". iDestruct (own_valid with "H") as %[[] _].
+  Qed.
 
   Lemma newlock_spec (R : iProp Σ) Φ :
     heapN ⊥ N →
-    heap_ctx ★ R ★ (∀ lk γs, is_lock γs lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
+    heap_ctx ★ R ★ (∀ lk γ, is_lock γ lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
   Proof.
     iIntros (HN) "(#Hh & HR & HΦ)". rewrite /newlock /=.
     wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
-    iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
-    iVs (own_alloc_strong (Auth (Excl' ∅) ∅) {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.
-    iVs (inv_alloc N _ (lock_inv γ1 γ2 lo ln R) with "[-HΦ]").
-    - iNext. rewrite /lock_inv.
-      iExists 0%nat, 0%nat.
-      iFrame.
-      iSplitL "Hγ1".
-      + rewrite /auth_inv.
-        iExists (GSet ∅).
-        by iFrame.
-      + iLeft. by iFrame.
-    - iVsIntro.
-      iApply ("HΦ" $! (#lo, #ln)%V (γ1, γ2)).
-      iExists lo, ln.
-      iSplit; by eauto.
+    iVs (own_alloc (● (Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']".
+    { by rewrite -auth_both_op. }
+    iVs (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
+    { iNext. rewrite /lock_inv.
+      iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
+    iVsIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
   Qed.
 
-  Lemma wait_loop_spec γs l x R (Φ : val → iProp Σ) :
-    issued γs l x R ★ (locked γs -★ R -★ Φ #()) ⊢ WP wait_loop #x l {{ Φ }}.
+  Lemma wait_loop_spec γ l x R (Φ : val → iProp Σ) :
+    issued γ l x R ★ (locked γ -★ R -★ Φ #()) ⊢ WP wait_loop #x l {{ Φ }}.
   Proof.
     iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
     iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
-    iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
+    iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
     wp_load. destruct (decide (x = o)) as [->|Hneq].
     - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
-      + iVs ("Hclose" with "[Hlo Hln Hainv Ht]").
+      + iVs ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
         { iNext. iExists o, n. iFrame. eauto. }
         iVsIntro. wp_let. wp_op=>[_|[]] //.
         wp_if. iVsIntro.
-        iApply ("HΦ" with "[-HR] HR"). eauto.
+        iApply ("HΦ" with "[-HR] HR"). rewrite /locked; eauto.
       + iExFalso. iCombine "Ht" "Haown" as "Haown".
-        iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
+        iDestruct (own_valid with "Haown") as % [_ ?%gset_disj_valid_op].
         set_solver.
     - iVs ("Hclose" with "[Hlo Hln Ha]").
       { iNext. iExists o, n. by iFrame. }
@@ -126,64 +110,72 @@ Section proof.
       wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
   Qed.
 
-  Lemma acquire_spec γs l R (Φ : val → iProp Σ) :
-    is_lock γs l R ★ (locked γs -★ R -★ Φ #()) ⊢ WP acquire l {{ Φ }}.
+  Lemma acquire_spec γ l R (Φ : val → iProp Σ) :
+    is_lock γ l R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire l {{ Φ }}.
   Proof.
     iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
     iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
     iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
-    wp_load. iVs ("Hclose" with "[Hlo Hln Ha]").
+    wp_load. iVs ("Hclose" with "[Hlo Hln Ha]") as "_".
     { iNext. iExists o, n. by iFrame. }
     iVsIntro. wp_let. wp_proj. wp_op.
     wp_bind (CAS _ _ _).
-    iInv N as (o' n') "[Hlo' [Hln' [Hainv Haown]]]" "Hclose".
+    iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)" "Hclose".
     destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
     - wp_cas_suc.
-      iDestruct "Hainv" as (s) "[Ho %]"; subst.
-      iVs (own_update with "Ho") as "Ho".
-      { eapply auth_update_no_frag, (gset_disj_alloc_empty_local_update n).
-        rewrite elem_of_seq_set; omega. }
-      iDestruct "Ho" as "[Hofull Hofrag]".
-      iVs ("Hclose" with "[Hlo' Hln' Haown Hofull]").
-      { rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
+      iVs (own_update with "Hauth") as "Hauth".
+      { eapply (auth_update_no_frag _ (∅, _)), prod_local_update,
+          (gset_disj_alloc_empty_local_update n); [done|].
+        rewrite elem_of_seq_set. omega. }
+      rewrite pair_op left_id_L. iDestruct "Hauth" as "[Hauth Hofull]".
+      rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
       rewrite -(seq_set_S_union_L 0).
-        iNext. iExists o', (S n)%nat.
-        rewrite Nat2Z.inj_succ -Z.add_1_r.
-        iFrame. iExists (GSet (seq_set 0 (S n))). by iFrame. }
+      iVs ("Hclose" with "[Hlo' Hln' Haown Hauth]") as "_".
+      { iNext. iExists o', (S n).
+        rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
       iVsIntro. wp_if.
-      iApply (wait_loop_spec γs (#lo, #ln)).
-      iSplitR "HΦ"; last by auto.
-      rewrite /issued /auth_own; eauto 10.
+      iApply (wait_loop_spec γ (#lo, #ln)).
+      iFrame "HΦ". rewrite /issued; eauto 10.
     - wp_cas_fail.
-      iVs ("Hclose" with "[Hlo' Hln' Hainv Haown]").
+      iVs ("Hclose" with "[Hlo' Hln' Hauth Haown]").
       { iNext. iExists o', n'. by iFrame. }
       iVsIntro. wp_if. by iApply "IH".
   Qed.
 
-  Lemma release_spec γs l R (Φ : val → iProp Σ):
-    is_lock γs l R ★ locked γs ★ R ★ Φ #() ⊢ WP release l {{ Φ }}.
+  Lemma release_spec γ l R (Φ : val → iProp Σ):
+    is_lock γ l R ★ locked γ ★ R ★ Φ #() ⊢ WP release l {{ Φ }}.
   Proof.
-    iIntros "(Hl & Hγ & HR & HΦ)". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
-    iLöb as "IH". wp_rec. subst. wp_proj. wp_bind (! _)%E.
-    iInv N as (o n) "[Hlo [Hln Hr]]" "Hclose".
-    wp_load. iVs ("Hclose" with "[Hlo Hln Hr]").
+    iIntros "(Hl & Hγ & HR & HΦ)".
+    iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
+    iDestruct "Hγ" as (o) "Hγo".
+    rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
+    iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
+    wp_load.
+    iAssert (o' = o)%I with "[#]" as "%"; subst.
+    { iCombine "Hγo" "Hauth" as "Hγo".
+      by iDestruct (own_valid with "Hγo") (* FIXME: this is horrible *)
+        as %[[[[?|] ?] [=]%leibniz_equiv_iff] ?]%auth_valid_discrete. }
+    iVs ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
     { iNext. iExists o, n. by iFrame. }
-    iVsIntro. wp_let. wp_bind (CAS _ _ _ ).
-    wp_proj. wp_op.
-    iInv N as (o' n') "[Hlo' [Hln' Hr]]" "Hclose".
-    destruct (decide (#o' = #o))%V as [[= ->%Nat2Z.inj ] | Hneq].
-    - wp_cas_suc.
-      iDestruct "Hr" as "[Hainv [[Ho _] | Hown]]".
-      + iExFalso. iCombine "Hγ" "Ho" as "Ho".
-        iDestruct (own_valid with "#Ho") as %[].
-      + iVs ("Hclose" with "[Hlo' Hln' HR Hγ Hainv]").
-        { iNext. iExists (o + 1)%nat, n'%nat.
-          iFrame. rewrite Nat2Z.inj_add.
-          iFrame. iLeft; by iFrame. }
-        iVsIntro. by wp_if.
-    - wp_cas_fail. iVs ("Hclose" with "[Hlo' Hln' Hr]").
-      { iNext. iExists o', n'. by iFrame. }
-      iVsIntro. wp_if. by iApply ("IH" with "Hγ HR").
+    iVsIntro. wp_op.
+    iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
+    wp_store.
+    iAssert (o' = o)%I with "[#]" as "%"; subst.
+    { iCombine "Hγo" "Hauth" as "Hγo".
+      by iDestruct (own_valid with "Hγo")
+        as %[[[[?|] ?] [=]%leibniz_equiv_iff] ?]%auth_valid_discrete. }
+    iDestruct "Haown" as "[[Hγo' _]|?]".
+    { iCombine "Hγo" "Hγo'" as "Hγo".
+      iDestruct (own_valid with "#Hγo") as %[[] ?]. }
+    iCombine "Hauth" "Hγo" as "Hauth".
+    iVs (own_update with "Hauth") as "Hauth".
+    { rewrite pair_split_L. apply: (auth_update _ _ (Excl' (S o), _)). (* FIXME: apply is slow *)
+      apply prod_local_update, reflexivity; simpl.
+      by apply option_local_update, exclusive_local_update. }
+    rewrite -pair_split_L. iDestruct "Hauth" as "[Hauth Hγo]".
+    iVs ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last auto.
+    iNext. iExists (S o), n'.
+    rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
   Qed.
 End proof.
 

[Robbert Krebbers]

Not sure whether my proof can be simplified. The purpose of the exclusive RA is to ensure that the value of owner is not changed in between the read and write in release.

@zhangz

[Ghost User]

Impressive, the new release is much more sensible now :) The old CAS loop is (unfortunately) introduced due to my reasoning that two "bump counter by 1" are somewhat symmetric, as well as the fact that I previously used a bundle value pair pointed by a single location instead of a pair of locations.

For further simplification, I imaged a new invariant like this (based on my previous definition):

  Definition lock_inv (γ1 γ2: gname) (lo ln: loc) (R : iProp Σ) : iProp Σ :=
    (∃ (o n: nat),
      ln ↦ #n ★
       auth_inv γ1 (tickets_inv n) ★
       ((( lo ↦ #o ★ own γ2 (Excl ()) ★ R) ∨ auth_own γ1 (GSet {[ o ]})))%I.

i.e. moving the lo's ownership to local control. So when we try to release, it is exclusively owned locally which saves the trouble of proving this fact. However, this can mess up the standard lock interface (EDIT: maybe not, we just need to prove locked to be exclusive).

As a side note, I am not sure the motivation behind turning a list of RAs into a product one (However, introducing a pair of ghost names is not very elegant, but it was easier to reason about for me at that time). So I'd like to hear some general comments on whether these two approaches are interchangeable and which one should we prefer in which case.

Thanks

[Robbert Krebbers]

The old CAS loop is (unfortunately) introduced due to my reasoning that two "bump counter by 1" are somewhat symmetric, as well as the fact that I previously used a bundle value pair pointed by a single location instead of a pair of locations.

I see.

i.e. moving the lo's ownership to local control. So when we try to release, it is exclusively owned locally which saves the trouble of proving this fact. However, this can mess up the standard lock interface (EDIT: maybe not, we just need to prove locked to be exclusive).

You can do that, but I am not sure whether it makes it easier: you somehow need to make the locked predicate be aware of the location. You can either do that by defining names to be pairs of locations and ghost names, or by using some ghost state.

As a side note, I am not sure the motivation behind turning a list of RAs into a product one (However, introducing a pair of ghost names is not very elegant, but it was easier to reason about for me at that time). So I'd like to hear some general comments on whether these two approaches are interchangeable and which one should we prefer in which case.

Note that in this case, I had to put the exclusive in the auth, so having two different ghost instances would be a bit awkward.