make the lock cancellable

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0429c257e3088cf77c8852a2cbeff2b02671b8b5
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 56f0afb23dc761c9a822a505d6d7d2cc435b681b

theories/lang/lib/lock.v

 From iris.program_logic Require Import weakestpre.
-From iris.base_logic.lib Require Import invariants.
+From iris.base_logic.lib Require Import cancelable_invariants.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
 From lrust.lang Require Import proofmode notation.
@@ -14,8 +14,8 @@ Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
 
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
-Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
-Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
+Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC); lock_cinvG :> cinvG Σ }.
+Definition lockΣ : gFunctors := #[GFunctor (exclR unitC); cinvΣ].
 
 Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
@@ -23,15 +23,20 @@ Proof. solve_inG. Qed.
 Section proof.
   Context `{!lrustG Σ, !lockG Σ} (N : namespace).
 
+  Definition lockname := (gname * gname)%type.
+
   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) (l : loc) (R : iProp Σ) : iProp Σ :=
-    (inv N (lock_inv γ l R))%I.
+  Definition is_lock (γ : lockname) (l : loc) (R : iProp Σ) : iProp Σ :=
+    (cinv N (γ.1) (lock_inv (γ.2) l R))%I.
+
+  Definition own_lock (γ : lockname) : frac → iProp Σ :=
+    cinv_own (γ.1).
 
-  Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
+  Definition locked (γ : lockname): iProp Σ := own (γ.2) (Excl ()).
 
-  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
+  Lemma locked_exclusive (γ : lockname) : locked γ -∗ locked γ -∗ False.
   Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
 
   Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
@@ -46,62 +51,71 @@ Section proof.
   Proof. apply _. Qed.
 
   Lemma newlock_inplace (E : coPset) (R : iProp Σ) l :
-    ▷ R -∗ l ↦ #false ={E}=∗ ∃ γ, is_lock γ l R.
+    ▷ R -∗ l ↦ #false ={E}=∗ ∃ γ, is_lock γ l R ∗ own_lock γ 1%Qp.
   Proof.
     iIntros "HR Hl".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
-    iMod (inv_alloc N _ (lock_inv γ l R) with "[-]") as "#?".
+    iMod (cinv_alloc _ N (lock_inv γ l R) with "[-]") as (γ') "Hlock".
     { iNext. iExists false. by iFrame. }
-    eauto.
+    iModIntro. iExists (_, _). eauto.
   Qed.
-    
 
   Lemma newlock_spec (R : iProp Σ) :
-    {{{ ▷ R }}} newlock [] {{{ l γ, RET #l; is_lock γ l R }}}.
+    {{{ ▷ R }}} newlock [] {{{ l γ, RET #l; is_lock γ l R ∗ own_lock γ 1%Qp }}}.
   Proof.
     iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
     wp_seq. wp_alloc l vl as "Hl" "H†". inv_vec vl=>x.
     (* FIXME: Something is wrong with the printing of the expression here *)
     rewrite heap_mapsto_vec_singleton. (* FIXME shouldn't this also compute now, like bigops do? *)
     wp_let. wp_write.
-    iMod (newlock_inplace with "[HR] Hl") as (γ) "?".
-    { (* FIXME: Can we make it so that we can just say "HR" instead of "[HR]", and the
-         later does not matter? Or at least, "$HR" should work.  Why can't we frame
-         below later? *)
-      done. }
+    iMod (newlock_inplace with "[HR //] Hl") as (γ) "?".
     iApply "HΦ". done.
   Qed.
 
-  Lemma try_acquire_spec γ l R :
-    {{{ is_lock γ l R }}} try_acquire [ #l ]
-    {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
+  Lemma destroy_lock E γ l R :
+    ↑N ⊆ E → 
+    is_lock γ l R -∗ own_lock γ 1%Qp ={E}=∗ ∃ (b : bool), l ↦ #b.
+  Proof.
+    iIntros (?) "#Hinv Hown".
+    iMod (cinv_cancel with "Hinv Hown") as (b) "[>Hl _]"; first done.
+    eauto.
+  Qed.
+
+  Lemma try_acquire_spec γ l R q :
+    {{{ is_lock γ l R ∗ own_lock γ q }}} try_acquire [ #l ]
+    {{{ b, RET #b; (if b is true then locked γ ∗ R else True) ∗ own_lock γ q }}}.
   Proof.
-    iIntros (Φ) "#Hinv HΦ".
-    wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
+    iIntros (Φ) "[Hinv Hown] HΦ".
+    wp_rec. iMod (cinv_open with "Hinv Hown") as "(Hinv & Hown & Hclose)"; first done.
+    iDestruct "Hinv" as ([]) "[Hl HR]".
     - wp_apply (wp_cas_int_fail with "Hl"); [done..|]. iIntros "Hl".
       iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
-      iModIntro. iApply ("HΦ" $! false). done.
+      iModIntro. iApply ("HΦ" $! false). auto.
     - wp_apply (wp_cas_int_suc with "Hl"); [done..|]. iIntros "Hl".
       iDestruct "HR" as "[Hγ HR]".
       iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
-      iModIntro. rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
+      iModIntro. rewrite /locked. iApply ("HΦ" $! true with "[$Hγ $HR $Hown]").
   Qed.
 
-  Lemma acquire_spec γ l R :
-    {{{ is_lock γ l R }}} acquire [ #l ] {{{ RET #(); locked γ ∗ R }}}.
+  Lemma acquire_spec γ l R q :
+    {{{ is_lock γ l R ∗ own_lock γ q }}} acquire [ #l ]
+    {{{ RET #(); locked γ ∗ R ∗ own_lock γ q }}}.
   Proof.
-    iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
-    wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
-    - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
-    - iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
+    iIntros (Φ) "[#Hinv Hown] HΦ". iLöb as "IH". wp_rec.
+    wp_apply (try_acquire_spec with "[$Hinv $Hown]"). iIntros ([]).
+    - iIntros "[[Hlked HR] Hown]". wp_if. iApply "HΦ"; iFrame.
+    - iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown [HΦ]"). auto.
   Qed.
 
-  Lemma release_spec γ l R :
-    {{{ is_lock γ l R ∗ locked γ ∗ R }}} release [ #l ] {{{ RET #(); True }}}.
+  Lemma release_spec γ l R q :
+    {{{ is_lock γ l R ∗ locked γ ∗ R ∗ own_lock γ q }}} release [ #l ]
+    {{{ RET #(); own_lock γ q }}}.
   Proof.
-    iIntros (Φ) "(#Hinv & Hlocked & HR) HΦ".
-    rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
-    wp_write. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
+    iIntros (Φ) "(Hinv & Hlocked & HR & Hown) HΦ".
+    rewrite /release /=. wp_let.
+    iMod (cinv_open with "Hinv Hown") as "(Hinv & Hown & Hclose)"; first done.
+    iDestruct "Hinv" as (b) "[? _]". wp_write. iApply "HΦ". iFrame "Hown".
+    iApply "Hclose". iNext. iExists false. by iFrame.
   Qed.
 End proof.