(** Concurrent bag specification from the HOCAP paper. "Modular Reasoning about Separation of Concurrent Data Structures" <http://www.kasv.dk/articles/hocap-ext.pdf> Coarse-grained implementation of a bag *) 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 cmra agree frac. From iris.heap_lang.lib Require Import lock spin_lock. From iris_examples.hocap Require Import abstract_bag. Set Default Proof Using "Type". (** Coarse-grained bag implementation using a spin lock *) Definition newBag : val := λ: <>, let: "r" := ref NONE in let: "l" := newlock #() in ("r", "l"). Definition pushBag : val := λ: "b" "v", let: "l" := Snd "b" in let: "r" := Fst "b" in acquire "l";; let: "t" := !"r" in "r" <- SOME ("v", "t");; release "l". Definition popBag : val := λ: "b", let: "l" := Snd "b" in let: "r" := Fst "b" in acquire "l";; let: "v" := match: !"r" with NONE => NONE | SOME "s" => "r" <- Snd "s";; SOME (Fst "s") end in release "l";; "v". Canonical Structure valmultisetC := leibnizC (gmultiset valC). Class bagG Σ := BagG { bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetC)); lock_bagG :> lockG Σ }. (** Generic specification for the bag, using view shifts. *) Section proof. Context `{heapG Σ, bagG Σ}. Variable N : namespace. Fixpoint bag_of_val (ls : val) : gmultiset val := match ls with | NONEV => ∅ | SOMEV (v1, t) => {[v1]} ∪ bag_of_val t | _ => ∅ end. Fixpoint val_of_list (ls : list val) : val := match ls with | [] => NONEV | x::xs => SOMEV (x, val_of_list xs) end. Definition bag_inv (γb : gname) (b : loc) : iProp Σ := (∃ ls : list val, b ↦ (val_of_list ls) ∗ own γb ((1/2)%Qp, to_agree (of_list ls)))%I. Definition is_bag (γb : gname) (x : val) := (∃ (lk : val) (b : loc) (γ : gname), ⌜x = PairV #b lk⌝ ∗ is_lock N γ lk (bag_inv γb b))%I. Definition bag_contents (γb : gname) (X : gmultiset val) : iProp Σ := own γb ((1/2)%Qp, to_agree X). Global Instance is_bag_persistent γb x : Persistent (is_bag γb x). Proof. apply _. Qed. Global Instance bag_contents_timeless γb X : Timeless (bag_contents γb X). Proof. apply _. Qed. Lemma bag_contents_agree γb X Y : bag_contents γb X -∗ bag_contents γb Y -∗ ⌜X = Y⌝. Proof. rewrite /bag_contents. apply bi.wand_intro_r. rewrite -own_op own_valid uPred.discrete_valid. f_equiv=> /=. rewrite pair_op. by intros [_ ?%agree_op_invL']. Qed. Lemma bag_contents_update γb X X' Y : bag_contents γb X ∗ bag_contents γb X' ==∗ bag_contents γb Y ∗ bag_contents γb Y. Proof. iIntros "[Hb1 Hb2]". iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-. iMod (own_update_2 with "Hb1 Hb2") as "Hb". { rewrite pair_op frac_op'. assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp_div_2. by apply (cmra_update_exclusive (1%Qp, to_agree Y)). } iDestruct "Hb" as "[Hb1 Hb2]". rewrite /bag_contents. by iFrame. Qed. Lemma newBag_spec : {{{ True }}} newBag #() {{{ x γ, RET x; is_bag γ x ∗ bag_contents γ ∅ }}}. Proof. iIntros (Φ) "_ HΦ". unfold newBag. wp_rec. wp_alloc r as "Hr". wp_let. iMod (own_alloc (1%Qp, to_agree ∅)) as (γb) "[Ha Hf]"; first done. wp_apply (newlock_spec N (bag_inv γb r) with "[Hr Ha]"). { iExists []. iFrame. } iIntros (lk γ) "#Hlk". wp_let. iApply "HΦ". rewrite /is_bag /bag_contents. iFrame. iExists _,_,_. by iFrame "Hlk". Qed. Local Opaque acquire release. (* so that wp_pure doesn't stumble *) Lemma pushBag_spec (P Q : iProp Σ) γ (x v : val) : □ (∀ (X : gmultiset val), bag_contents γ X ∗ P ={⊤∖↑N}=∗ ▷ (bag_contents γ ({[v]} ∪ X) ∗ Q)) -∗ {{{ is_bag γ x ∗ P }}} pushBag x (of_val v) {{{ RET #(); Q }}}. Proof. iIntros "#Hvs". iIntros (Φ). iAlways. iIntros "[#Hbag HP] HΦ". unfold pushBag. do 2 wp_rec. rewrite /is_bag /bag_inv. iDestruct "Hbag" as (lk b γl) "[% #Hlk]"; simplify_eq/=. repeat wp_pure _. wp_apply (acquire_spec with "Hlk"). iIntros "[Htok Hb1]". iDestruct "Hb1" as (ls) "[Hb Ha]". wp_seq. wp_load. wp_let. wp_bind (_ <- _)%E. iApply (wp_mask_mono _ (⊤∖↑N)); first done. iMod ("Hvs" with "[$Ha $HP]") as "[Hbc HQ]". wp_store. wp_let. wp_apply (release_spec with "[$Hlk $Htok Hbc Hb]"). { iExists (v::ls); iFrame. } iIntros "_". by iApply "HΦ". Qed. Lemma popBag_spec (P : iProp Σ) (Q : val → iProp Σ) γ x : □ (∀ (X : gmultiset val) (y : val), bag_contents γ ({[y]} ∪ X) ∗ P ={⊤∖↑N}=∗ ▷ (bag_contents γ X ∗ Q (SOMEV y))) -∗ □ (bag_contents γ ∅ ∗ P ={⊤∖↑N}=∗ ▷ (bag_contents γ ∅ ∗ Q NONEV)) -∗ {{{ is_bag γ x ∗ P }}} popBag x {{{ v, RET v; Q v }}}. Proof. iIntros "#Hvs1 #Hvs2". iIntros (Φ). iAlways. iIntros "[#Hbag HP] HΦ". unfold popBag. wp_rec. rewrite /is_bag /bag_inv. iDestruct "Hbag" as (lk b γl) "[% #Hlk]"; simplify_eq/=. repeat wp_pure _. wp_apply (acquire_spec with "Hlk"). iIntros "[Htok Hb1]". iDestruct "Hb1" as (ls) "[Hb Ha]". wp_seq. wp_bind (!#b)%E. iApply (wp_mask_mono _ (⊤∖↑N)); first done. destruct ls as [|v ls]; simpl. - iMod ("Hvs2" with "[$Ha $HP]") as "[Hbc HQ]". wp_load. repeat wp_pure _. wp_apply (release_spec with "[$Hlk $Htok Hbc Hb]"). { iExists []; iFrame. } iIntros "_". repeat wp_pure _. by iApply "HΦ". - iMod ("Hvs1" with "[$Ha $HP]") as "[Hbc HQ]". wp_load. repeat wp_pure _. wp_store. do 2 wp_pure _. wp_apply (release_spec with "[$Hlk $Htok Hbc Hb]"). { iExists ls; iFrame. } iIntros "_". repeat wp_pure _. by iApply "HΦ". Qed. End proof. Typeclasses Opaque bag_contents is_bag. Canonical Structure cg_bag `{!heapG Σ, !bagG Σ} : bag Σ := {| abstract_bag.is_bag := is_bag; abstract_bag.is_bag_persistent := is_bag_persistent; abstract_bag.bag_contents_timeless := bag_contents_timeless; abstract_bag.bag_contents_agree := bag_contents_agree; abstract_bag.bag_contents_update := bag_contents_update; abstract_bag.newBag_spec := newBag_spec; abstract_bag.pushBag_spec := pushBag_spec; abstract_bag.popBag_spec := popBag_spec |}.