Implement the cancellable locks specification

theories/c_translation/monad.v

@@ -42,20 +42,21 @@ Definition a_par : val := λ: "x" "y" "env" "l",
 Definition amonadN := nroot .@ "amonad".
 
 Section a_wp.
-  Context `{heapG Σ, lockG Σ, spawnG Σ}.
+  Context `{heapG Σ, flockG Σ, spawnG Σ}.
 
   Definition awp (e : expr)
       (R : iProp Σ) (Φ : val → iProp Σ) : iProp Σ :=
-    (∀ (γ : gname) (π : frac) (env : val) (l : val),
-      is_flock γ π false l (env_inv env ∗ R) -∗
+    (∀ (γ : flock_name) (π : frac) (env : val) (l : val),
+      is_flock amonadN γ l (env_inv env ∗ R) -∗
+      unflocked γ π -∗
       WP e env l {{ v,
-        Φ v ∗ is_flock γ π false l (env_inv env ∗ R) }}
+        Φ v ∗ unflocked γ π }}
     )%I.
 
   Lemma awp_ret e R Φ :
     WP e {{ Φ }} -∗ awp (a_ret e) R Φ.
   Proof.
-    iIntros "Hwp" (γ π env l) "Hlock".
+    iIntros "Hwp" (γ π env l) "#Hlock Hunfl".
     rewrite /a_ret. wp_bind e.
     iApply (wp_wand with "Hwp"); iIntros (v) "HΦ /=".
     do 3 wp_lam. iFrame.
@@ -65,11 +66,11 @@ Section a_wp.
   Lemma awp_bind (f v : val) R Φ :
     awp v R (λ w, awp (f w) R Φ) -∗ awp (a_bind f v) R Φ.
   Proof.
-    iIntros "Hwp" (γ π env l) "Hlock".
+    iIntros "Hwp" (γ π env l) "#Hlock Hunfl".
     rewrite /a_bind /=. do 4 wp_lam.
     wp_bind (v env l).
-    iApply (wp_wand with "[Hwp Hlock]"); first by iApply "Hwp".
-    iIntros (w) "[Hwp Hlock]". wp_let. by iApply "Hwp".
+    iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
+    iIntros (w) "[Hwp Hunfl]". wp_let. by iApply "Hwp".
   Qed.
 
   Lemma awp_run (v : val) R Φ :
@@ -89,39 +90,39 @@ Section a_wp.
   Qed.
 *) Admitted.
 
-  Lemma awp_atomic (v : val) R Φ :
-    (R -∗ ∃ R', R' ∗ awp v R' (λ w, R' -∗ R ∗ Φ w)) -∗
+  Lemma awp_atomic (v : val) R Φ `{Timeless _ R} :
+    (R -∗ ∃ R', ⌜Timeless R'⌝ ∧ R' ∗ awp v R' (λ w, R' -∗ R ∗ Φ w)) -∗
     awp (a_atomic v) R Φ.
   Proof.
-    iIntros "Hwp" (γ π env l) "Hlock1".
+    iIntros "Hwp" (γ π env l) "#Hlock1 Hunfl1".
     rewrite /a_atomic /=. do 3 wp_let.
     wp_apply (acquire_cancel_spec with "[$]").
-    iIntros "[Hlock1 [Henv HR]] /=". wp_seq.
-    iDestruct ("Hwp" with "HR") as (R') "[HR' Hwp]".
-    wp_apply (newlock_cancel_spec (env_inv env ∗ R')%I with "[$Henv $HR']").
-    iIntros (k γ') "Hlock2". wp_let. wp_bind (v env k).
-    iApply (wp_wand with "[Hwp Hlock2]"); first by iApply "Hwp".
-    iIntros (w) "[HR Hlock2]". wp_let.
-    iMod (cancel_lock with "Hlock2") as "[Henv HR']".
+    iIntros "[Hflkd [Henv HR]] /=". wp_seq.
+    iDestruct ("Hwp" with "HR") as (R') "(% & HR' & Hwp)".
+    wp_apply (newlock_cancel_spec amonadN (env_inv env ∗ R')%I with "[$Henv $HR']").
+    iIntros (k γ') "[#Hlock2 Hunfl2]". wp_let. wp_bind (v env k).
+    iApply (wp_wand with "[Hwp Hunfl2]"); first by iApply "Hwp".
+    iIntros (w) "[HR Hunfl2]". wp_let.
+    iMod (cancel_lock with "Hlock2 Hunfl2") as "[Henv HR']".
     iDestruct ("HR" with "HR'") as "[HR HΦ]".
-    wp_apply (release_cancel_spec with "[$Hlock1 $Henv $HR]").
-    iIntros "Hlock1". wp_seq. iFrame.
+    wp_apply (release_cancel_spec with "[$Hlock1 $Hflkd $Henv $HR]").
+    iIntros "Hunfl1". wp_seq. iFrame.
   Qed.
 
-  Lemma awp_atomic_env (v : val) R Φ :
+  Lemma awp_atomic_env (v : val) R Φ `{Timeless _ R} :
     (∀ env, env_inv env -∗ R -∗
       WP v env {{ w, env_inv env ∗ R ∗ Φ w }}) -∗
     awp (a_atomic_env v) R Φ.
   Proof.
-    iIntros "Hwp" (γ π env l) "Hlock".
+    iIntros "Hwp" (γ π env l) "#Hlock Hunfl".
     rewrite /a_atomic_env /=. do 3 wp_lam.
     wp_apply (acquire_cancel_spec with "[$]").
-    iIntros "[Hlock1 [Henv HR]] /=". wp_seq.
+    iIntros "[Hflkd [Henv HR]] /=". wp_seq.
     iDestruct ("Hwp" with "Henv HR") as "Hwp".
     wp_apply (wp_wand with "Hwp").
     iIntros (w) "[Henv [HR HΦ]]". wp_let.
-    wp_apply (release_cancel_spec with "[$Hlock1 $Henv $HR]").
-    iIntros "Hlock". wp_seq. iFrame.
+    wp_apply (release_cancel_spec with "[$Hlock $Hflkd $Henv $HR]").
+    iIntros "Hunfl". wp_seq. iFrame.
   Qed.
 
   Lemma awp_par (v1 v2 : val) R (Ψ1 Ψ2 Φ : val → iProp Σ) :
@@ -130,11 +131,11 @@ Section a_wp.
     ▷ (∀ w1 w2, Ψ1 w1 -∗ Ψ2 w2 -∗ ▷ Φ (w1,w2)%V) -∗
     awp (a_par v1 v2) R Φ.
   Proof.
-    iIntros "Hwp1 Hwp2 HΦ" (γ π env l) "[Hlock1 Hlock2]".
+    iIntros "Hwp1 Hwp2 HΦ" (γ π env l) "#Hlock [Hunfl1 Hunfl2]".
     rewrite /a_par /=. do 4 wp_lam.
-    iApply (par_spec (λ v, Ψ1 v ∗ is_flock γ _ false l _)%I
-                     (λ v, Ψ2 v ∗ is_flock γ _ false l _)%I
-      with "[Hwp1 Hlock1] [Hwp2 Hlock2]").
+    iApply (par_spec (λ v, Ψ1 v ∗ unflocked _ (π/2))%I
+                     (λ v, Ψ2 v ∗ unflocked _ (π/2))%I
+      with "[Hwp1 Hunfl1] [Hwp2 Hunfl2]").
     - wp_lam. by iApply "Hwp1".
     - wp_lam. by iApply "Hwp2".
     - iNext. iIntros (w1 w2) "[[HΨ1 $] [HΨ2 $]]".

theories/lib/flock.v

+(** Cancellable locks *)
 From iris.heap_lang Require Export proofmode notation.
-From iris.heap_lang Require Import spin_lock assert par.
-From iris.algebra Require Import frac.
+From iris.heap_lang Require Import spin_lock.
+From iris.base_logic.lib Require Import cancelable_invariants.
+From iris.algebra Require Import auth excl frac.
 From iris.base_logic.lib Require Import fractional.
 
+Inductive lockstate :=
+  | Locked : frac → lockstate
+  | Unlocked.
+Canonical Structure lockstateC := leibnizC lockstate.
+
+Record flock_name := {
+  flock_lock_name : gname;
+  flock_cinv_name : gname;
+  flock_state_name : gname;
+}.
+
+Class flockG Σ :=
+  FlockG {
+    flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
+    flock_cinvG :> cinvG Σ;
+    flock_lockG :> lockG Σ
+  }.
+
+
+Section cinv_lemmas.
+  Context `{invG Σ, cinvG Σ}.
+
+  Lemma cinv_alloc_strong (G : gset gname) E N (Φ : gname → iProp Σ) :
+    ▷ (∀ γ, ⌜γ ∉ G⌝ → Φ γ) ={E}=∗ ∃ γ, ⌜γ ∉ G⌝ ∧ cinv N γ (Φ γ) ∗ cinv_own γ 1.
+  Proof.
+    iIntros "HP".
+    iMod (own_alloc_strong 1%Qp G) as (γ) "[% H1]"; first done.
+    iMod (inv_alloc N _ (Φ γ ∨ own γ 1%Qp)%I with "[HP]") as "#Hinv".
+    - iNext. iLeft. by iApply "HP".
+    - iExists γ. iModIntro. rewrite /cinv /cinv_own. iFrame "H1".
+      iSplit; eauto. iExists _. iFrame "Hinv".
+      iIntros "!# !>". iSplit; by iIntros "?".
+  Qed.
+
+  Lemma cinv_cancel_vs (P Q : iProp Σ) E N γ :
+    ↑N ⊆ E → cinv N γ P
+    -∗ (cinv_own γ 1 ∗ ▷ P ={E∖↑N}=∗ cinv_own γ 1 ∗ ▷ Q)
+    -∗ cinv_own γ 1 ={E}=∗ ▷ Q.
+  Proof.
+    iIntros (?) "#Hinv Hvs Hγ". rewrite /cinv.
+    iDestruct "Hinv" as (P') "[#HP' Hinv]".
+    iInv N as "[HP|>Hγ']" "Hclose"; last first.
+    - iDestruct (cinv_own_1_l with "Hγ Hγ'") as %[].
+    - iMod ("Hvs" with "[$Hγ HP]") as "[Hγ HQ]".
+      { by iApply "HP'". }
+      iFrame. iApply "Hclose". iNext. by iRight.
+  Qed.
+
+End cinv_lemmas.
+
 Section flock.
-  Context `{heapG Σ, lockG Σ, spawnG Σ}.
-
-  Definition is_flock (γ : gname) (π : frac) (b : bool)
-             (l : val) (R : iProp Σ) : iProp Σ.
-  Admitted.
-
-  Lemma is_flock_op γ π1 π2 lk R :
-    is_flock γ (π1 + π2) false lk R ⊣⊢
-      is_flock γ π1 false lk R ∗ is_flock γ π2 false lk R.
-  Proof. Admitted.
-
-  Global Instance is_flock_fractional γ lk R :
-    Fractional (λ π, is_flock γ π false lk R).
-  Proof. intros p q. apply is_flock_op. Qed.
-  Global Instance is_flock_as_fractional γ π lk R :
-    AsFractional (is_flock γ π false lk R) (λ π, is_flock γ π false lk R) π.
+  Context `{heapG Σ, flockG Σ}.
+
+  Variable N : namespace.
+
+  Definition flock_inv (γ : flock_name) (R : iProp Σ) : iProp Σ :=
+    (∃ s : lockstate,
+       own (flock_state_name γ) (● (Excl' s)) ∗
+       match s with
+       | Locked q =>
+         cinv_own (flock_cinv_name γ) (q/2) ∗
+         locked (flock_lock_name γ)
+       | Unlocked => R
+       end)%I.
+
+  Local Instance flock_inv_timeless γ R `{Timeless _ R} : Timeless (flock_inv γ R).
+  Proof.
+    rewrite /flock_inv.
+    apply uPred.exist_timeless => s.
+    destruct s; apply _.
+  Qed.
+
+  Definition is_flock (γ : flock_name) (lk : val) (R : iProp Σ) : iProp Σ :=
+    (cinv (N .@ "inv") (flock_cinv_name γ) (flock_inv γ R) ∗
+     is_lock (N .@ "lock") (flock_lock_name γ) lk
+         (own (flock_state_name γ) (◯ (Excl' Unlocked))))%I.
+
+  Global Instance is_flock_persistent γ lk R : Persistent (is_flock γ lk R).
+  Proof. apply _. Qed.
+
+  Definition unflocked (γ : flock_name) (q : frac) : iProp Σ :=
+    cinv_own (flock_cinv_name γ) q.
+
+  Definition flocked (γ : flock_name) (q : frac) : iProp Σ :=
+    (own (flock_state_name γ) (◯ (Excl' (Locked q)))
+     ∗ cinv_own (flock_cinv_name γ) (q/2))%I.
+
+  Lemma unflocked_op (γ : flock_name) (π1 π2 : frac) :
+    unflocked γ (π1+π2) ⊣⊢
+      unflocked γ π1 ∗ unflocked γ π2.
+  Proof. by rewrite /unflocked fractional. Qed.
+
+  Global Instance unflocked_fractional γ :
+    Fractional (unflocked γ).
+  Proof. intros p q. apply unflocked_op. Qed.
+  Global Instance unflocked_as_fractional γ π :
+    AsFractional (unflocked γ π) (unflocked γ) π.
   Proof. split. done. apply _. Qed.
 
   Lemma newlock_cancel_spec (R : iProp Σ):
-    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_flock γ 1 false lk R }}}.
-  Proof. Admitted.
-
-  Lemma acquire_cancel_spec γ π lk R :
-    {{{ is_flock γ π false lk R }}} acquire lk
-    {{{ RET #(); is_flock γ π true lk R ∗ R }}}.
-  Proof. Admitted.
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk R ∗ unflocked γ 1 }}}.
+  Proof.
+    iIntros (Φ) "HR HΦ". rewrite -wp_fupd.
+    iMod (own_alloc (● (Excl' Unlocked) ⋅ ◯ (Excl' Unlocked)))
+      as (γ_state) "[Hauth Hfrag]"; first done.
+    iApply (newlock_spec (N.@"lock") (own γ_state (◯ (Excl' Unlocked))) with "Hfrag").
+    iNext. iIntros (lk γ_lock) "#Hlock".
+    iMod (cinv_alloc_strong ∅ _ (N.@"inv")
+       (fun γ => flock_inv (Build_flock_name γ_lock γ γ_state) R) with "[-HΦ]") as (γ_cinv) "(_ & #Hcinv & Hown)".
+    { iNext. rewrite /flock_inv /=. iIntros (γ _).
+      iExists Unlocked. by iFrame. }
+    pose (γ := (Build_flock_name γ_lock γ_cinv γ_state)).
+    iModIntro. iApply ("HΦ" $! lk γ). iFrame "Hown".
+    rewrite /is_flock. by iFrame "Hlock".
+  Qed.
 
-  Lemma release_cancel_spec γ π lk R :
-    {{{ is_flock γ π true lk R ∗ R }}} release lk
-    {{{ RET #(); is_flock γ π false lk R }}}.
-  Proof. Admitted.
+  Lemma acquire_cancel_spec γ π lk (R : iProp Σ) `{Timeless _ R} :
+    {{{ is_flock γ lk R ∗ unflocked γ π }}}
+      acquire lk
+    {{{ RET #(); flocked γ π ∗ R }}}.
+  Proof.
+    iIntros (Φ) "[Hl Hunfl] HΦ". rewrite -wp_fupd.
+    rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
+    iApply (acquire_spec with "Hlk"). iNext.
+    iIntros "[Hlocked Hunlk]".
+    iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first done.
+    rewrite {2}/flock_inv.
+    (* TODO: why doesn't this work?
+       iDestruct "Hstate" as (s) "Hstate". *)
+    iDestruct "Hstate" as ">Hstate".
+    iDestruct "Hstate" as (s) "Hstate".
+    destruct s as [q|].
+    - iDestruct "Hstate" as "(Hstate & Hcown & Hlocked2)".
+      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
+    - iDestruct "Hstate" as "[Hstate HR]".
+      iMod (own_update_2 with "Hstate Hunlk") as "Hstate".
+      { apply (auth_update _ _ (Excl' (Locked π)) (Excl' (Locked π))).
+        apply option_local_update.
+        by apply exclusive_local_update. }
+      iDestruct "Hstate" as "[Hstate Hflkd]".
+      iDestruct "Hunfl" as "[Hunfl Hcown]".
+      iMod ("Hcl" with "[Hstate Hcown Hlocked]").
+      { iNext. iExists (Locked π). iFrame. }
+      iApply "HΦ". by iFrame.
+  Qed.
 
-  Lemma cancel_lock γ lk R :
-    is_flock γ 1 false lk R ={⊤}=∗ R.
-  Proof. Admitted.
+  Lemma release_cancel_spec γ π lk R `{Timeless _ R} :
+    {{{ is_flock γ lk R ∗ flocked γ π ∗ R }}}
+      release lk
+    {{{ RET #(); unflocked γ π }}}.
+  Proof.
+    iIntros (Φ) "(Hl & (Hstate' & Hflkd) & HR) HΦ". rewrite -fupd_wp.
+    rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
+    iMod (cinv_open with "Hcinv Hflkd") as "(Hstate & Hunfl & Hcl)"; first done.
+    rewrite {2}/flock_inv.
+    (* TODO: why doesn't this work?
+       iDestruct "Hstate" as (s) "Hstate". *)
+    iDestruct "Hstate" as ">Hstate".
+    iDestruct "Hstate" as (s) "Hstate".
+    destruct s as [q|]; last first.
+    - iDestruct "Hstate" as "[Hstate HR']".
+      iExFalso. iDestruct (own_valid_2 with "Hstate Hstate'") as %Hfoo.
+      iPureIntro. revert Hfoo.
+      rewrite auth_valid_discrete /= left_id.
+      intros [Hexcl _].
+      apply Some_included_exclusive in Hexcl; try (done || apply _).
+      simplify_eq.
+    - iDestruct "Hstate" as "(Hstate & Hcown & Hlocked)".
+      iAssert (⌜q = π⌝)%I with "[Hstate Hstate']" as  %->.
+      { iDestruct (own_valid_2 with "Hstate Hstate'") as %Hfoo.
+        iPureIntro. revert Hfoo.
+        rewrite auth_valid_discrete /= left_id.
+        intros [Hexcl _].
+        apply Some_included_exclusive in Hexcl; try (done || apply _).
+        by simplify_eq. }
+      iMod (own_update_2 with "Hstate Hstate'") as "Hstate".
+      { apply (auth_update _ _ (Excl' Unlocked) (Excl' Unlocked)).
+        apply option_local_update.
+        by apply exclusive_local_update. }
+      iDestruct "Hstate" as "[Hstate Hstate']".
+      iMod ("Hcl" with "[Hstate HR]").
+      { iNext. iExists Unlocked. iFrame. }
+      iApply (release_spec with "[$Hlk $Hlocked $Hstate']").
+      iModIntro. iNext. iIntros "_". iApply "HΦ".
+      by iSplitL "Hcown".
+  Qed.
 
+  Lemma cancel_lock γ lk R `{Timeless _ R} :
+    is_flock γ lk R -∗ unflocked γ 1 ={⊤}=∗ R.
+  Proof.
+    rewrite /is_flock /unflocked.
+    iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "Hcown".
+    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as ">$"; eauto.
+    iIntros "[Hcown Hstate]".
+    iDestruct "Hstate" as ">Hstate".
+    iDestruct "Hstate" as (s) "(Hstate & HR)".
+    destruct s as [q|].
+    - iDestruct "HR" as "(Hcown2 & Hlocked)".
+      iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
+    - by iFrame.
+  Qed.
 
 End flock.