Flock v 2

_CoqProject

@@ -2,6 +2,7 @@
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 
 theories/lib/mset.v
+theories/lib/spin_lock.v
 theories/lib/flock.v
 theories/lib/locking_heap.v
 theories/lib/U.v

theories/c_translation/monad.v

@@ -2,6 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import adequacy spin_lock assert par.
 From iris.algebra Require Import frac.
 From iris_c.lib Require Import mset flock locking_heap.
+From iris.bi Require Import fractional.
 
 (* M A := ref (list loc) → Mutex → A *)
 
@@ -19,7 +20,10 @@ Notation "a ;;; b" := (a_bind (λ: <>, b) a)%E (at level 80, right associativity
 Definition a_run : val := λ: "x",
   let: "env" := mset_create #() in
   let: "l" := newlock #() in
-  "x" "env" "l".
+  let: "v" := "x" "env" "l"
+  in "v". (* TODO: we have a dummy step here :(
+             but potentially we would have a free(l) operation here
+           *)
 
 (* M A → M A *)
 Definition a_atomic : val := λ: "x" "env" "l",
@@ -67,9 +71,8 @@ Section a_wp.
       (R : iProp Σ) (Φ : val → iProp Σ) : iProp Σ :=
     tc_opaque (WP e {{ ev, ∀ (γ : flock_name) (π : frac) (env : val) (l : val),
       is_flock amonadN γ l -∗
-      flock_res γ (env_inv env ∗ R) -∗
-      unflocked γ π -∗
-      WP ev env l {{ v, Φ v ∗ unflocked γ π }}
+      flock_res γ (env_inv env ∗ R) π -∗
+      WP ev env l {{ v, Φ v ∗ flock_res γ (env_inv env ∗ R) π }}
     }})%I.
 
   Global Instance elim_bupd_awp p e Φ :
@@ -104,20 +107,21 @@ Section a_wp_rules.
 
   Lemma awp_insert_res e Φ R1 R2 :
     ▷ R1 -∗
-    awp e (R1 ∗ R2) Φ -∗
+    awp e (R1 ∗ R2) (λ v, R1 -∗ Φ v) -∗
     awp e R2 Φ.
   Proof.
     iIntros "HR1 Hawp". rewrite /awp /=.
     iApply (wp_wand with "Hawp").
     iIntros (v) "HΦ".
-    iIntros (γ π env l) "#Hflock Hres Hunfl".
-    iMod (flock_res_insert_unflocked with "Hflock Hres Hunfl HR1")
-      as "(#Hres & Hunfl)"; first done.
-    iApply ("HΦ" with "Hflock [Hres] Hunfl").
-    rewrite (comm (∗)%I R1 R2).
-    rewrite (assoc (∗)%I _ R2 R1).
-    by iFrame "Hres".
-  Qed.
+    iIntros (γ π env l) "#Hflock Hres".
+  (*   iMod (flock_res_insert_unflocked with "Hflock Hres Hunfl HR1") *)
+  (*     as "(#Hres & Hunfl)"; first done. *)
+  (*   iApply ("HΦ" with "Hflock [Hres] Hunfl"). *)
+  (*   rewrite (comm (∗)%I R1 R2). *)
+  (*   rewrite (assoc (∗)%I _ R2 R1). *)
+  (*   by iFrame "Hres". *)
+  (* Qed. *)
+  Abort.
 
   Lemma awp_wand e (Φ Ψ : val → iProp Σ) R :
     awp e R Φ -∗
@@ -127,8 +131,8 @@ Section a_wp_rules.
     iIntros "HAWP Hv". rewrite /awp /=.
     iApply (wp_wand with "HAWP").
     iIntros (v) "HΦ".
-    iIntros (γ π env l) "#Hflock #Hres Hunfl".
-    iApply (wp_wand with "[HΦ Hunfl]"); first by iApply "HΦ".
+    iIntros (γ π env l) "#Hflock Hres".
+    iApply (wp_wand with "[HΦ Hres]"); first by iApply "HΦ".
     iIntros (w) "[HΦ $]". by iApply "Hv".
   Qed.
 
@@ -147,7 +151,7 @@ Section a_wp_rules.
   Proof.
     iIntros "Hwp". rewrite /awp /a_ret /=. wp_apply (wp_wand with "Hwp").
     iIntros (v) "HΦ". wp_lam.
-    iIntros (γ π env l) "#Hlock #Hres Hunfl". do 2 wp_lam. iFrame.
+    iIntros (γ π env l) "#Hlock Hres". do 2 wp_lam. iFrame.
   Qed.
 
   Lemma awp_bind (f e : expr) R Φ :
@@ -157,53 +161,63 @@ Section a_wp_rules.
   Proof.
     iIntros ([fv <-%of_to_val]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e.
     iApply (wp_wand with "Hwp"). iIntros (ev) "Hwp". wp_lam.
-    iIntros (γ π env l) "#Hlock #Hres Hunfl". do 2 wp_lam. wp_bind (ev env l).
-    iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
-    iIntros (w) "[Hwp Hunfl]". wp_let. wp_apply (wp_wand with "Hwp").
+    iIntros (γ π env l) "#Hlock Hres". do 2 wp_lam. wp_bind (ev env l).
+    iApply (wp_wand with "[Hwp Hres]"); first by iApply "Hwp".
+    iIntros (w) "[Hwp Hres]". wp_let. wp_apply (wp_wand with "Hwp").
     iIntros (v) "H". by iApply ("H" with "[$]").
   Qed.
 
   Lemma awp_atomic (e : expr) (ev : val) R Φ :
     IntoVal e ev →
-    (R -∗ ∃ R', R' ∗ awp (ev #()) R' (λ w, R' -∗ R ∗ Φ w)) -∗
+    ▷ (R -∗ ∃ R', R' ∗ awp (ev #()) R' (λ w, R' -∗ R ∗ Φ w)) -∗
     awp (a_atomic e) R Φ.
   Proof.
     iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic /=. wp_lam.
-    iIntros (γ π env l) "#Hlock1 #Hres Hunfl1". do 2 wp_let.
+    iIntros (γ π env l) "#Hlock1 Hres". do 2 wp_let.
     wp_apply (acquire_cancel_spec with "[$]").
-    iIntros (f) "([Henv HR] & Hcl)". wp_seq.
-    iDestruct ("Hwp" with "HR") as (R') "[HR' Hwp]".
+    iDestruct 1 as (R') "(HR' & #Heq & Hcl)". wp_seq.
+    iAssert (▷ (env_inv env ∗ R))%I with "[HR']" as "[Henv HR]".
+    { iNext. iRewrite "Heq". done. } 
+    iDestruct ("Hwp" with "HR") as (Q) "[HQ Hwp]".
     wp_apply (newlock_cancel_spec amonadN); first done.
-    iIntros (k γ') "[#Hlock2 Hunfl2]". wp_let.
-    iMod (flock_res_alloc_unflocked _ _ _ _ (env_inv env ∗ R')%I
-            with "Hlock2 Hunfl2 [$Henv $HR']") as "[#Hres2 Hunfl2]"; first done.
+    iIntros (k γ') "#Hlock2".
+    iMod (flock_res_single_alloc _ _ _ (env_inv env ∗ Q)%I
+            with "Hlock2 [$Henv $HQ]") as "Hres"; first done.
+    wp_let.
     wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
-    iApply (wp_wand with "[Hwp Hunfl2]"); first by iApply "Hwp".
-    iIntros (w) "[HR Hunfl2]".
-    iMod (cancel_lock with "Hlock2 Hres2 Hunfl2") as "[Henv HR']"; first done.
+    iApply (wp_wand with "[Hwp Hres]"); first by iApply "Hwp".
+    iIntros (w) "[HR Hres]".
+    iMod (flock_res_single_dealloc with "Hlock2 Hres") as (Q') "[HQ' #HeqQ]"; first done.
     wp_let.
-    iDestruct ("HR" with "HR'") as "[HR HΦ]".
-    wp_apply (release_cancel_spec with "[$Hlock1 Hcl Henv HR]").
-    { iApply "Hcl". by iNext; iFrame. }
-    iIntros "Hunfl1". wp_seq. iFrame.
+    iAssert (▷ (env_inv env ∗ Q))%I with "[HQ']" as "[Henv HQ]".
+    { iNext. by iRewrite "HeqQ". }
+    iDestruct ("HR" with "HQ") as "[HR HΦ]".
+    iAssert (▷ R')%I with "[HR Henv]" as "HR'".
+    { iNext. iRewrite -"Heq". iFrame. }
+    iMod ("Hcl" with "HR'") as "[Hflocked Hres]".
+    wp_apply (release_cancel_spec with "[$Hlock1 $Hflocked]").
+    iIntros "_". wp_seq. iFrame.
   Qed.
 
   Lemma awp_atomic_env (e : expr) (ev : val) R Φ :
     IntoVal e ev →
-    (∀ env, env_inv env -∗ R -∗
-      WP ev env {{ w, env_inv env ∗ R ∗ Φ w }}) -∗
+    (∀ env, ▷ env_inv env -∗ ▷ R -∗
+        WP ev env {{ w, env_inv env ∗ R ∗ Φ w }}) -∗
     awp (a_atomic_env e) R Φ.
   Proof.
     iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam.
-    iIntros (γ π env l) "#Hlock #Hres Hunfl". do 2 wp_lam.
+    iIntros (γ π env l) "#Hlock Hres". do 2 wp_lam.
     wp_apply (acquire_cancel_spec with "[$]").
-    iIntros (f) "([Henv HR] & Hcl)". wp_seq.
+    iDestruct 1 as (R') "(HR' & #Heq & Hcl)". wp_seq.
+    iAssert (▷ (env_inv env ∗ R))%I with "[HR']" as "[Henv HR]".
+    { iNext. iRewrite "Heq". done. }
     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 "[$Hlock Hcl Henv HR]").
-    { iApply "Hcl". by iNext; iFrame. }
-    iIntros "Hunfl". wp_seq. iFrame.
+    iRewrite -"Heq" in "Hcl".
+    iMod ("Hcl" with "[$HR $Henv]") as "[Hflocked Hres]".
+    wp_apply (release_cancel_spec with "[$Hlock $Hflocked]").
+    iIntros "_". wp_seq. iFrame.
   Qed.
 
   Lemma awp_par (Ψ1 Ψ2 : val → iProp Σ) e1 e2 R (Φ : val → iProp Σ) :
@@ -217,12 +231,12 @@ Section a_wp_rules.
     iIntros (ev1) "Hwp1". wp_lam.
     wp_bind e2. iApply (wp_wand with "Hwp2").
     iIntros (ev2) "Hwp2". wp_lam.
-    iIntros (γ π env l) "#Hlock #Hres [Hunfl1 Hunfl2]". do 2 wp_lam.
-    iApply (par_spec (λ v, Ψ1 v ∗ unflocked _ (π/2))%I
-                     (λ v, Ψ2 v ∗ unflocked _ (π/2))%I
-      with "[Hwp1 Hunfl1] [Hwp2 Hunfl2]").
-    - wp_lam. iApply ("Hwp1" with "Hlock Hres Hunfl1").
-    - wp_lam. iApply ("Hwp2" with "Hlock Hres Hunfl2").
+    iIntros (γ π env l) "#Hlock [Hres1 Hres2]". do 2 wp_lam.
+    iApply (par_spec (λ v, Ψ1 v ∗ flock_res _ _ (π/2))%I
+                     (λ v, Ψ2 v ∗ flock_res _ _ (π/2))%I
+      with "[Hwp1 Hres1] [Hwp2 Hres2]").
+    - wp_lam. iApply ("Hwp1" with "Hlock Hres1").
+    - wp_lam. iApply ("Hwp2" with "Hlock Hres2").
     - iNext. iIntros (w1 w2) "[[HΨ1 $] [HΨ2 $]]".
       iApply ("HΦ" with "[$] [$]").
   Qed.
@@ -233,7 +247,7 @@ Section a_wp_run.
 
   Lemma awp_run (e : expr) R Φ :
     AsVal e →
-    R -∗ (∀ `{amonadG Σ}, awp e R (λ w, ▷ R ={⊤}=∗ Φ w)) -∗
+    ▷ R -∗ (∀ `{amonadG Σ}, awp e R (λ w, ▷ R ={⊤}=∗ Φ w)) -∗
     WP a_run e {{ Φ }}.
   Proof.
     iIntros ([ev <-%of_to_val]) "HR Hwp". rewrite /awp /a_run /=. wp_let.
@@ -242,16 +256,18 @@ Section a_wp_run.
     iMod (locking_heap_init ∅) as (?) "Hσ".
     pose (amg := AMonadG Σ _ _ _ _).
     wp_apply (newlock_cancel_spec amonadN); first done.
-    iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd.
-    iMod (flock_res_alloc_unflocked _ _ _ _ (env_inv env ∗ R)%I
-            with "Hlock Hunfl [Henv Hσ $HR]") as "[#Hres Hunfl]"; first done.
+    iIntros (k γ') "#Hlock". rewrite- wp_fupd.
+    iMod (flock_res_single_alloc _ _ _ (env_inv env ∗ R)%I
+            with "Hlock [Henv Hσ $HR]") as "Hres"; first done.
     { iNext. iExists ∅, ∅. iFrame. eauto. }
     iSpecialize ("Hwp" $! amg).
-    wp_apply (wp_wand with "Hwp"). iIntros (v') "Hwp".
-    iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
-    iIntros (w) "[HΦ Hunfl]".
-    iMod (cancel_lock with "Hlock Hres Hunfl") as "[HEnv HR]"; first done.
-    by iApply "HΦ".
+    iMod (wp_value_inv with "Hwp") as "Hwp".
+    wp_let. wp_bind (ev env k).    
+    iApply (wp_wand with "[Hwp Hres]"); first by iApply "Hwp".
+    iIntros (w) "[HΦ Hres]".
+    iMod (flock_res_single_dealloc with "Hlock Hres") as (R') "[HR' #Heq]"; first done.
+    wp_let.
+    iApply "HΦ". iNext. iRewrite -"Heq" in "HR'". iDestruct "HR'" as "[_ $]".
   Qed.
 End a_wp_run.
 

theories/c_translation/translation.v

@@ -67,10 +67,10 @@ Section proofs.
     iApply awp_atomic_env.
     iIntros (env) "Henv HR".
     rewrite {2}/env_inv.
-    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
+    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". wp_lam.
     iDestruct "Hlocks" as %Hlocks.
     iApply wp_fupd.
-    wp_let. wp_alloc l as "Hl".
+    wp_alloc l as "Hl".
     iAssert (⌜σ !! l = None⌝)%I with "[Hl Hls]" as %Hl.
     { remember (σ !! l) as σl. destruct σl; simplify_eq; eauto.
       iExFalso. rewrite (big_sepM_lookup _ σ l _); last eauto.
@@ -101,13 +101,13 @@ Section proofs.
     iApply awp_atomic_env.
     iIntros (env) "Henv HR".
     rewrite {2}/env_inv.
-    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
+    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". wp_lam.
     iDestruct "Hlocks" as %Hlocks.
     iDestruct (locked_locs_unlocked with "Hv Hσ") as %Hl.
     assert (#l ∉ X).
     { unfold correct_locks in *. intros Hx. apply Hl.
       destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
-    wp_let. wp_proj.
+    wp_proj.
     wp_apply (mset_add_spec with "[$HX]"); eauto.
     iIntros "HX". wp_seq.
     iAssert (⌜σ !! l = Some ULvl⌝%I) with "[Hσ Hv]" as %?.
@@ -148,13 +148,12 @@ Section proofs.
     iApply awp_atomic_env.
     iIntros (env) "Henv HR".
     rewrite {2}/env_inv.
-    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
+    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". wp_lam.
     iDestruct "Hlocks" as %Hlocks.
     iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hl.
     assert (#l ∉ X).
     { unfold correct_locks in *. intros Hx. apply Hl.
       destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
-    wp_let.
     wp_apply wp_assert.
     wp_apply (mset_member_spec #l env with "HX").
     iIntros "Henv /=". case_decide; first by exfalso. simpl.
@@ -204,9 +203,9 @@ Section proofs.
     iIntros (env) "Henv HR".
     iApply wp_fupd.
     rewrite {2}/env_inv.
-    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
+    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". wp_lam.
     iDestruct "Hlocks" as %Hlocks.
-    wp_let. iApply (mset_clear_spec with "HX").
+    iApply (mset_clear_spec with "HX").
     iNext. iIntros "HX".
     iDestruct "HΦ" as (us) "[Hus HΦ]".
     clear Hlocks.
@@ -279,7 +278,7 @@ Section proofs.
     iSpecialize ("Hfa" with "HΨ").
     iModIntro.
     awp_let.
-    iApply awp_atomic. iIntros "HR".
+    iApply awp_atomic. iNext. iIntros "HR".
     iDestruct ("Hfa" with "HR") as (R') "[HR' Hfa]".
     iExists R'. iFrame. by awp_let.
   Qed.

theories/lib/spin_lock.v

+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+From iris.algebra Require Import excl.
+From iris.heap_lang.lib Require Import lock.
+Set Default Proof Using "Type".
+
+Definition newlock : val := λ: <>, ref #false.
+Definition try_acquire : val := λ: "l", CAS "l" #false #true.
+Definition acquire : val :=
+  rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
+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)].
+
+Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Proof. solve_inG. Qed.
+
+Section proof.
+  Context `{!heapG Σ, !lockG Σ} (N : namespace).
+
+  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 locked (γ : gname) : iProp Σ := own γ (Excl ()).
+
+  Lemma locked_exclusive (γ : gname) : 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).
+  Proof. solve_proper. Qed.
+  Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
+  Proof. solve_proper. Qed.
+
+  (** The main proofs. *)
+  Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
+  Proof. apply _. Qed.
+  Global Instance locked_timeless γ : Timeless (locked γ).
+  Proof. apply _. Qed.
+
+  Lemma newlock_spec (R : iProp Σ):
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
+  Proof.
+    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
+    wp_lam. wp_alloc l as "Hl".
+    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
+    iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
+    { iIntros "!>". iExists false. by iFrame. }
+    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 }}}.
+  Proof.
+    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
+    wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
+    - wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+      iModIntro. iApply ("HΦ" $! false). done.
+    - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
+      iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+      iModIntro. rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
+  Qed.
+
+  Lemma acquire_spec γ lk R :
+    (∀ Φ,
+      is_lock γ lk R -∗ ▷ (locked γ ∗ R -∗ |={⊤}=> ▷ Φ #()%V) -∗ WP acquire lk {{ Φ }})%I.
+  Proof.
+    iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
+    wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
+    - iIntros "[Hlked HR]". iMod ("HΦ" with "[$Hlked $HR]"). wp_if. done.
+    - iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
+  Qed.
+
+  Lemma release_spec γ lk R :
+    {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
+  Proof.
+    iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
+    iDestruct "Hlock" as (l ->) "#Hinv".
+    rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
+    wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
+  Qed.
+End proof.
+
+Typeclasses Opaque is_lock locked.
+