Get rid of γs in locks.

theories/heap_lang/lib/lock.v

@@ -8,32 +8,29 @@ Structure lock Σ `{!heapG Σ} := Lock {
   acquire : val;
   release : val;
   (* -- predicates -- *)
-  (* name is used to associate locked with is_lock *)
-  name : Type;
-  is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
-  locked (γ: name) : iProp Σ;
+  is_lock (N: namespace) (lk: val) (R: iProp Σ) : iProp Σ;
+  locked (lk: val) : iProp Σ;
   (* -- general properties -- *)
-  is_lock_ne N γ lk : NonExpansive (is_lock N γ lk);
-  is_lock_persistent N γ lk R : Persistent (is_lock N γ lk R);
-  locked_timeless γ : Timeless (locked γ);
-  locked_exclusive γ : locked γ -∗ locked γ -∗ False;
+  is_lock_ne N lk : NonExpansive (is_lock N lk);
+  is_lock_persistent N lk R : Persistent (is_lock N lk R);
+  locked_timeless lk : Timeless (locked lk);
+  locked_exclusive lk : locked lk -∗ locked lk -∗ False;
   (* -- operation specs -- *)
   newlock_spec N (R : iProp Σ) :
-    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
-  acquire_spec N γ lk R :
-    {{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}};
-  release_spec N γ lk R :
-    {{{ is_lock N γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}
+    {{{ R }}} newlock #() {{{ lk, RET lk; is_lock N lk R }}};
+  acquire_spec N lk R :
+    {{{ is_lock N lk R }}} acquire lk {{{ RET #(); locked lk ∗ R }}};
+  release_spec N lk R :
+    {{{ is_lock N lk R ∗ locked lk ∗ R }}} release lk {{{ RET #(); True }}}
 }.
 
 Arguments newlock {_ _} _.
 Arguments acquire {_ _} _.
 Arguments release {_ _} _.
-Arguments is_lock {_ _} _ _ _ _ _.
+Arguments is_lock {_ _} _ _ _ _.
 Arguments locked {_ _} _ _.
 
 Existing Instances is_lock_ne is_lock_persistent locked_timeless.
 
-Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N γ lk:
-  Proper ((≡) ==> (≡)) (is_lock L N γ lk) := ne_proper _.
-
+Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N lk:
+  Proper ((≡) ==> (≡)) (is_lock L N lk) := ne_proper _.

theories/heap_lang/lib/spin_lock.v

@@ -26,51 +26,58 @@ Section proof.
   Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
     (∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I.
 
-  Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
-    (∃ l: loc, ⌜lk = #l⌝ ∧ inv N (lock_inv γ l R))%I.
+  Definition is_lock (lk : val) (R : iProp Σ) : iProp Σ :=
+    (∃ γ (l: loc), ⌜lk = #l⌝ ∧ meta l nroot γ ∧ inv N (lock_inv γ l R))%I.
 
-  Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
+  Definition locked (lk : val) : iProp Σ :=
+    (∃ γ (l: loc), ⌜lk = #l⌝ ∧ meta l nroot γ ∧ own γ (Excl ()))%I.
 
-  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
-  Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
+  Lemma locked_exclusive lk : locked lk -∗ locked lk -∗ False.
+  Proof.
+    iDestruct 1 as (γ1 l1 ?) "[#Hm1 H1]".
+    iDestruct 1 as (γ2 l2 ?) "[#Hm2 H2]"; simplify_eq/=.
+    iDestruct (meta_agree with "Hm1 Hm2") as %<-.
+    by iDestruct (own_valid_2 with "H1 H2") as %?.
+  Qed.
 
-  Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
+  Global Instance lock_inv_ne γ lk : NonExpansive (lock_inv γ lk).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
+  Global Instance is_lock_ne lk : NonExpansive (is_lock lk).
   Proof. solve_proper. Qed.
 
   (** The main proofs. *)
-  Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
+  Global Instance is_lock_persistent lk R : Persistent (is_lock lk R).
   Proof. apply _. Qed.
-  Global Instance locked_timeless γ : Timeless (locked γ).
+  Global Instance locked_timeless lk : Timeless (locked lk).
   Proof. apply _. Qed.
 
   Lemma newlock_spec (R : iProp Σ):
-    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
+    {{{ R }}} newlock #() {{{ lk, RET lk; is_lock lk R }}}.
   Proof.
     iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
-    wp_lam. wp_alloc l as "Hl".
+    wp_lam. wp_apply (wp_alloc with "[//]"); iIntros (l) "[Hl Hm]".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
+    iMod (meta_set _ _ γ nroot with "Hm") as "#Hm"; first done.
     iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
     { iIntros "!>". iExists false. by iFrame. }
-    iModIntro. iApply "HΦ". iExists l. eauto.
+    iModIntro. iApply "HΦ". iExists γ, l. eauto.
   Qed.
 
-  Lemma try_acquire_spec γ lk R :
-    {{{ is_lock γ lk R }}} try_acquire lk
-    {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
+  Lemma try_acquire_spec lk R :
+    {{{ is_lock lk R }}} try_acquire lk
+    {{{ b, RET #b; if b is true then locked lk ∗ R else True }}}.
   Proof.
-    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
+    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (γ l ->) "#[Hm Hinv]".
     wp_rec. iInv N as ([]) "[Hl HR]".
     - wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
       iApply ("HΦ" $! false). done.
     - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
       iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
-      rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
+      rewrite /locked. iApply ("HΦ" $! true with "[$HR Hγ]"); eauto.
   Qed.
 
-  Lemma acquire_spec γ lk R :
-    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}.
+  Lemma acquire_spec lk R :
+    {{{ is_lock lk R }}} acquire lk {{{ RET #(); locked lk ∗ R }}}.
   Proof.
     iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
     wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
@@ -78,11 +85,13 @@ Section proof.
     - iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
   Qed.
 
-  Lemma release_spec γ lk R :
-    {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
+  Lemma release_spec lk R :
+    {{{ is_lock lk R ∗ locked lk ∗ R }}} release lk {{{ RET #(); True }}}.
   Proof.
     iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
-    iDestruct "Hlock" as (l ->) "#Hinv".
+    iDestruct "Hlock" as (γ l ->) "#[Hm Hinv]".
+    iDestruct "Hlocked" as (γ' l' ?) "[#Hm' Hlocked]"; simplify_eq/=.
+    iDestruct (meta_agree with "Hm Hm'") as %<-.
     rewrite /release /=. wp_lam. iInv N as (b) "[Hl _]".
     wp_store. iSplitR "HΦ"; last by iApply "HΦ".
     iModIntro. iNext. iExists false. by iFrame.

theories/heap_lang/lib/ticket_lock.v

@@ -45,48 +45,56 @@ Section proof.
       own γ (● (Excl' o, GSet (set_seq 0 n))) ∗
       ((own γ (◯ (Excl' o, GSet ∅)) ∗ R) ∨ own γ (◯ (ε, GSet {[ o ]}))))%I.
 
-  Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
-    (∃ lo ln : loc,
-       ⌜lk = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln R))%I.
+  Definition is_lock (lk : val) (R : iProp Σ) : iProp Σ :=
+    (∃ γ (lo ln : loc),
+       ⌜lk = (#lo, #ln)%V⌝ ∗ meta lo nroot γ ∗ inv N (lock_inv γ lo ln R))%I.
 
-  Definition issued (γ : gname) (x : nat) : iProp Σ :=
-    own γ (◯ (ε, GSet {[ x ]}))%I.
+  Definition issued (lk : val) (x : nat) : iProp Σ :=
+    (∃ γ (lo ln : loc),
+       ⌜lk = (#lo, #ln)%V⌝ ∗ meta lo nroot γ ∗ own γ (◯ (ε, GSet {[ x ]})))%I.
 
-  Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, GSet ∅)))%I.
+  Definition locked (lk : val) : iProp Σ :=
+    (∃ γ (lo ln : loc) o,
+       ⌜lk = (#lo, #ln)%V⌝ ∗ meta lo nroot γ ∗ own γ (◯ (Excl' o, GSet ∅)))%I.
 
   Global Instance lock_inv_ne γ lo ln :
     NonExpansive (lock_inv γ lo ln).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_ne γ lk : NonExpansive (is_lock γ lk).
+  Global Instance is_lock_ne lk : NonExpansive (is_lock lk).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_persistent γ lk R : Persistent (is_lock γ lk R).
+  Global Instance is_lock_persistent lk R : Persistent (is_lock lk R).
   Proof. apply _. Qed.
-  Global Instance locked_timeless γ : Timeless (locked γ).
+  Global Instance locked_timeless lk : Timeless (locked lk).
   Proof. apply _. Qed.
 
-  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
+  Lemma locked_exclusive lk : locked lk -∗ locked lk -∗ False.
   Proof.
-    iDestruct 1 as (o1) "H1". iDestruct 1 as (o2) "H2".
+    iDestruct 1 as (γ1 lo1 ln1 o1 ?) "[#Hm1 H1]".
+    iDestruct 1 as (γ2 lo2 ln2 o2 ?) "[#Hm2 H2]"; simplify_eq/=.
+    iDestruct (meta_agree with "Hm1 Hm2") as %<-.
     iDestruct (own_valid_2 with "H1 H2") as %[[] _].
   Qed.
 
   Lemma newlock_spec (R : iProp Σ) :
-    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
+    {{{ R }}} newlock #() {{{ lk, RET lk; is_lock lk R }}}.
   Proof.
     iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
-    wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
+    wp_alloc ln as "Hln". wp_apply (wp_alloc with "[//]"); iIntros (lo) "[Hlo Hm]".
     iMod (own_alloc (● (Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
     { by apply auth_both_valid. }
+    iMod (meta_set _ _ γ nroot with "Hm") as "#Hm"; first done.
     iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
     { iNext. rewrite /lock_inv.
       iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
-    wp_pures. iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
+    wp_pures. iModIntro. iApply ("HΦ" $! (#lo, #ln)%V). iExists γ, lo, ln. eauto.
   Qed.
 
-  Lemma wait_loop_spec γ lk x R :
-    {{{ is_lock γ lk R ∗ issued γ x }}} wait_loop #x lk {{{ RET #(); locked γ ∗ R }}}.
+  Lemma wait_loop_spec lk x R :
+    {{{ is_lock lk R ∗ issued lk x }}} wait_loop #x lk {{{ RET #(); locked lk ∗ R }}}.
   Proof.
-    iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
+    iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (γ lo' ln' ->) "#[Hm Hinv]".
+    iDestruct "Ht" as (γ' lo ln ?) "[#Hm' Ht]"; simplify_eq/=.
+    iDestruct (meta_agree with "Hm Hm'") as %<-.
     iLöb as "IH". wp_rec. subst. wp_pures. wp_bind (! _)%E.
     iInv N as (o n) "(Hlo & Hln & Ha)".
     wp_load. destruct (decide (x = o)) as [->|Hneq].
@@ -94,7 +102,7 @@ Section proof.
       + iModIntro. iSplitL "Hlo Hln Hainv Ht".
         { iNext. iExists o, n. iFrame. }
         wp_pures. case_bool_decide; [|done]. wp_if.
-        iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
+        iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto 20.
       + iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
         set_solver.
     - iModIntro. iSplitL "Hlo Hln Ha".
@@ -103,10 +111,10 @@ Section proof.
       wp_if. iApply ("IH" with "Ht"). iNext. by iExact "HΦ".
   Qed.
 
-  Lemma acquire_spec γ lk R :
-    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}.
+  Lemma acquire_spec lk R :
+    {{{ is_lock lk R }}} acquire lk {{{ RET #(); locked lk ∗ R }}}.
   Proof.
-    iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
+    iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (γ lo ln ->) "#[Hm Hinv]".
     iLöb as "IH". wp_rec. wp_bind (! _)%E. simplify_eq/=. wp_proj.
     iInv N as (o n) "[Hlo [Hln Ha]]".
     wp_load. iModIntro. iSplitL "Hlo Hln Ha".
@@ -123,8 +131,8 @@ Section proof.
       { iNext. iExists o', (S n).
         rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
       wp_if.
-      iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
-      + iFrame. rewrite /is_lock; eauto 10.
+      iApply (wait_loop_spec (#lo, #ln) with "[-HΦ]").
+      + iFrame. rewrite /is_lock /issued; eauto 20.
       + by iNext.
     - wp_cas_fail. iModIntro.
       iSplitL "Hlo' Hln' Hauth Haown".
@@ -132,11 +140,12 @@ Section proof.
       wp_if. by iApply "IH"; auto.
   Qed.
 
-  Lemma release_spec γ lk R :
-    {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
+  Lemma release_spec lk R :
+    {{{ is_lock lk R ∗ locked lk ∗ R }}} release lk {{{ RET #(); True }}}.
   Proof.
-    iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
-    iDestruct "Hγ" as (o) "Hγo".
+    iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (γ' lo' ln' ->) "#[Hm Hinv]".
+    iDestruct "Hγ" as (γ lo ln o ?) "[#Hm' Hγo]"; simplify_eq/=.
+    iDestruct (meta_agree with "Hm Hm'") as %<-.
     wp_lam. wp_proj. wp_bind (! _)%E.
     iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
     wp_load.