Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
(** 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 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).
Global Instance bag_contents_timeless γb X : Timeless (bag_contents γb X).
Lemma bag_contents_agree γb X Y :
bag_contents γb X -∗ bag_contents γb Y -∗ ⌜X = Y⌝.
rewrite /bag_contents. 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 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]".
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".
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 /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.
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_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.
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_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 |}.