Commit b92b197b authored by Dan Frumin's avatar Dan Frumin

Add the concurrent bag example from the HOCAP paper

parent 9c9943a2
......@@ -69,3 +69,8 @@ theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
theories/hocap/abstract_bag.v
theories/hocap/cg_bag.v
theories/hocap/exclusive_bag.v
theories/hocap/shared_bag.v
(** Concurrent bag specification from the HOCAP paper.
"Modular Reasoning about Separation of Concurrent Data Structures"
<http://www.kasv.dk/articles/hocap-ext.pdf>
This file: abstract bag specification
*)
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
From stdpp Require Import gmultiset.
Set Default Proof Using "Type".
Structure bag Σ `{!heapG Σ} := Bag {
(* -- operations -- *)
newBag : val;
pushBag : val;
popBag : val;
(* -- predicates -- *)
(* name is used to associate locked with is_lock *)
name : Type;
is_bag (N: namespace) (γ: name) (b: val) : iProp Σ;
bag_contents (γ: name) (X: gmultiset val) : iProp Σ;
(* -- ghost state theory -- *)
is_bag_persistent N γ b : Persistent (is_bag N γ b);
bag_contents_timeless γ X : Timeless (bag_contents γ X);
bag_contents_agree γ X Y: bag_contents γ X - bag_contents γ Y - X = Y;
bag_contents_update γ X X' Y:
bag_contents γ X bag_contents γ X' ==
bag_contents γ Y bag_contents γ Y;
(* -- operation specs -- *)
newBag_spec N :
{{{ True }}} newBag #() {{{ x γ, RET x; is_bag N γ x bag_contents γ }}};
pushBag_spec N P Q γ b v :
( (X : gmultiset val), bag_contents γ X P
={}= (bag_contents γ ({[v]} X) Q)) -
{{{ is_bag N γ b P }}}
pushBag b (of_val v)
{{{ RET #(); Q }}};
popBag_spec N P Q γ b :
( (X : gmultiset val) (y : val),
bag_contents γ ({[y]} X) P
={}= (bag_contents γ X Q (SOMEV y))) -
(bag_contents γ P ={}= (bag_contents γ Q NONEV)) -
{{{ is_bag N γ b P }}}
popBag b
{{{ v, RET v; Q v }}};
}.
Arguments newBag {_ _} _.
Arguments popBag {_ _} _.
Arguments pushBag {_ _} _.
Arguments newBag_spec {_ _} _ _ _.
Arguments popBag_spec {_ _} _ _ _ _ _ _.
Arguments pushBag_spec {_ _} _ _ _ _ _ _ _.
Arguments is_bag {_ _} _ _ _ _.
Arguments bag_contents {_ _} _ _.
Arguments bag_contents_update {_ _} _ {_ _ _}.
Existing Instances is_bag_persistent bag_contents_timeless.
(** 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 := λ: <>,
(ref NONE, newlock #()).
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 isBag (γb : gname) (x : val) :=
( (lk : val) (b : loc) (γ : gname),
x = PairV #b lk is_lock N γ lk (bag_inv γb b))%I.
Definition bagContents (γb : gname) (X : gmultiset val) : iProp Σ :=
own γb ((1/2)%Qp, to_agree X).
Global Instance isBag_persistent γb x : Persistent (isBag γb x).
Proof. apply _. Qed.
Global Instance bagContents_timeless γb X : Timeless (bagContents γb X).
Proof. apply _. Qed.
Lemma bagContents_agree γb X Y :
bagContents γb X - bagContents γb Y - X = Y.
Proof.
rewrite /bagContents. apply uPred.wand_intro_r.
rewrite -own_op own_valid uPred.discrete_valid.
f_equiv=> /=. rewrite pair_op.
by intros [_ ?%agree_op_invL'].
Qed.
Lemma bagContents_update γb X X' Y :
bagContents γb X bagContents γb X' == bagContents γb Y bagContents γb Y.
Proof.
iIntros "[Hb1 Hb2]".
iDestruct (bagContents_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 /bagContents. by iFrame.
Qed.
Lemma newBag_spec :
{{{ True }}}
newBag #()
{{{ x γ, RET x; isBag γ x bagContents γ }}}.
Proof.
iIntros (Φ) "_ HΦ".
unfold newBag. wp_rec.
wp_alloc r as "Hr".
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".
iApply wp_value. iApply "HΦ".
rewrite /isBag /bagContents. 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), bagContents γ X P
={}= (bagContents γ ({[v]} X) Q)) -
{{{ isBag γ 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 /isBag /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.
(* iApply (wp_mask_mono _ (⊤∖↑N)); first done. *)
iMod ("Hvs" with "[$Ha $HP]") as "[Hbc HQ]".
wp_store.
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),
bagContents γ ({[y]} X) P
={}= (bagContents γ X Q (SOMEV y))) -
(bagContents γ P ={}= (bagContents γ Q NONEV)) -
{{{ isBag γ x P }}}
popBag x
{{{ v, RET v; Q v }}}.
Proof.
iIntros "#Hvs1 #Hvs2".
iIntros (Φ). iAlways. iIntros "[#Hbag HP] HΦ".
unfold popBag. wp_rec.
rewrite /isBag /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. destruct ls as [|v ls]; simpl.
- iMod ("Hvs2" with "[$Ha $HP]") as "[Hbc HQ]".
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]".
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 bagContents isBag.
Canonical Structure cg_bag `{!heapG Σ, !bagG Σ} : bag Σ :=
{| is_bag := isBag;
is_bag_persistent := isBag_persistent;
bag_contents_timeless := bagContents_timeless;
bag_contents_agree := bagContents_agree;
bag_contents_update := bagContents_update;
abstract_bag.newBag_spec := newBag_spec;
abstract_bag.pushBag_spec := pushBag_spec;
abstract_bag.popBag_spec := popBag_spec |}.
(** Concurrent bag specification from the HOCAP paper.
"Modular Reasoning about Separation of Concurrent Data Structures"
<http://www.kasv.dk/articles/hocap-ext.pdf>
Deriving the sequential specification from the abstract one
*)
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_examples.hocap Require Import abstract_bag.
Set Default Proof Using "Type".
Section proof.
Context `{heapG Σ}.
Variable b : bag Σ.
Variable N : namespace.
Definition bagE (γ : name Σ b) (x : val) (X : gmultiset val) : iProp Σ :=
(is_bag b N γ x bag_contents b γ X)%I.
Lemma newBag_spec :
{{{ True }}}
newBag b #()
{{{ x, RET x; γ, bagE γ x }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply newBag_spec; eauto.
iNext. iIntros (x γ) "[#Hbag Hb]". iApply "HΦ".
iExists γ; by iFrame.
Qed.
Lemma pushBag_spec γ x X v :
{{{ bagE γ x X }}}
pushBag b x (of_val v)
{{{ RET #(); bagE γ x ({[v]} X) }}}.
Proof.
iIntros (Φ) "Hbag HΦ".
iApply (pushBag_spec b N (bagE γ x X)%I (bagE γ x ({[v]} X))%I with "[] [Hbag]"); eauto.
{ iAlways. iIntros (Y) "[Hb1 Hb2]".
iDestruct "Hb2" as "[#Hbag Hb2]".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iMod (bag_contents_update b ({[v]} Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
by iFrame. }
{ iDestruct "Hbag" as "[#Hbag Hb]". iFrame "Hbag". eauto. }
Qed.
Lemma popBag_spec γ x X :
{{{ bagE γ x X }}}
popBag b x
{{{ v, RET v; (X = ∅⌝ v = NONEV bagE γ x )
( Y y, X = {[y]} Y v = SOMEV y bagE γ x Y)}}}.
Proof.
iIntros (Φ) "Hbag HΦ".
iApply (popBag_spec b N (bagE γ x X)%I (fun v => (X = ∅⌝ v = NONEV bagE γ x )
( Y y, X = {[y]} Y v = SOMEV y bagE γ x Y))%I γ with "[] [] [Hbag]"); eauto.
{ iAlways. iIntros (Y y) "[Hb1 Hb2]".
iDestruct "Hb2" as "[#Hbag Hb2]".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iMod (bag_contents_update b Y with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
iFrame. iRight. iModIntro. iExists _,_; repeat iSplit; eauto. }
{ iAlways. iIntros "[Hb1 Hb2]".
iDestruct "Hb2" as "[#Hbag Hb2]".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iModIntro. iFrame. iLeft. repeat iSplit; eauto. }
{ iDestruct "Hbag" as "[#Hbag Hb]". iFrame "Hbag". eauto. }
Qed.
End proof.
(** Concurrent bag specification from the HOCAP paper.
"Modular Reasoning about Separation of Concurrent Data Structures"
<http://www.kasv.dk/articles/hocap-ext.pdf>
Deriving the concurrent specification from the abstract one
*)
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_examples.hocap Require Import abstract_bag.
Set Default Proof Using "Type".
Section proof.
Context `{heapG Σ}.
Variable b : bag Σ.
Variable N : namespace.
Variable N2 : namespace.
Variable P : val iProp Σ. (* Predicate that will be satisfied by all the elements in the bag *)
Definition bagS_inv (γ : name Σ b) : iProp Σ :=
inv N2 ( X, bag_contents b γ X [ mset] x X, P x)%I.
Definition bagS (γ : name Σ b) (x : val) : iProp Σ :=
(is_bag b N γ x bagS_inv γ)%I.
Global Instance bagS_persistent γ x : Persistent (bagS γ x).
Proof. apply _. Qed.
Lemma newBag_spec :
{{{ True }}}
newBag b #()
{{{ x, RET x; γ, bagS γ x }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_fupd.
iApply (newBag_spec b N); eauto.
iNext. iIntros (v γ) "[#Hbag Hcntn]".
iMod (inv_alloc N2 _ ( X, bag_contents b γ X [ mset] x X, P x)%I with "[Hcntn]") as "#Hinv".
{ iNext. iExists _. iFrame. by rewrite big_sepMS_empty. }
iApply "HΦ". iModIntro. iExists _; by iFrame "Hinv".
Qed.
Lemma pushBag_spec γ x v :
{{{ bagS γ x P v }}}
pushBag b x (of_val v)
{{{ RET #(); bagS γ x }}}.
Proof.
iIntros (Φ) "[#[Hbag Hinv] HP] HΦ". rewrite /bagS_inv.
iApply (pushBag_spec b N (P v)%I (True)%I with "[] [Hbag HP]"); eauto.
{ iAlways. iIntros (Y) "[Hb1 HP]".
iInv N2 as (X) "[>Hb2 HPs]" "Hcl".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iMod (bag_contents_update b ({[v]} Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
iFrame. iApply "Hcl".
iNext. iExists _; iFrame.
rewrite big_sepMS_union big_sepMS_singleton. iFrame. }
{ iNext. iIntros "_". iApply "HΦ". by iFrame "Hinv". }
Qed.
Lemma popBag_spec γ x :
{{{ bagS γ x }}}
popBag b x
{{{ v, RET v; bagS γ x (v = NONEV ( y, v = SOMEV y P y)) }}}.
Proof.
iIntros (Φ) "[#Hbag #Hinv] HΦ".
iApply (popBag_spec b N (True)%I (fun v => (v = NONEV ( y, v = SOMEV y P y)))%I with "[] [] [Hbag]"); eauto.
{ iAlways. iIntros (Y y) "[Hb1 _]".
iInv N2 as (X) "[>Hb2 HPs]" "Hcl".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iMod (bag_contents_update b Y with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
rewrite big_sepMS_union uPred.later_sep big_sepMS_singleton.
iDestruct "HPs" as "[HP HPs]".
iMod ("Hcl" with "[-HP Hb1]") as "_".
{ iNext. iExists _; iFrame. }
iModIntro. iNext. iFrame. iRight; eauto. }
{ iAlways. iIntros "[Hb1 _]".
iModIntro. iNext. iFrame. iLeft; eauto. }
{ iNext. iIntros (v) "H". iApply "HΦ". iFrame "Hinv Hbag H". }
Qed.
End proof.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment