exclusive_bag.v 2.66 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(** 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.

Dan Frumin's avatar
Dan Frumin committed
19
  (** An exclusive specification keeps track of the exact contents of the bag *)
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35
  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)
36
    {{{ RET #(); bagE γ x ({[v]}  X) }}}.
37 38
  Proof.
    iIntros (Φ) "Hbag HΦ".
39
    iApply (pushBag_spec b N (bagE γ x X)%I (bagE γ x ({[v]}  X))%I with "[] [Hbag]"); eauto.
40 41 42
    { iAlways. iIntros (Y) "[Hb1 Hb2]".
      iDestruct "Hb2" as "[#Hbag Hb2]".
      iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
43
      iMod (bag_contents_update b ({[v]}  Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
44 45 46 47 48 49 50 51
      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 )
52
                  ( Y y, X = {[y]}  Y  v = SOMEV y  bagE γ x Y)}}}.
53 54 55
  Proof.
    iIntros (Φ) "Hbag HΦ".
    iApply (popBag_spec b N (bagE γ x X)%I (fun v => (X = ∅⌝  v = NONEV  bagE γ x )
56
                  ( Y y, X = {[y]}  Y  v = SOMEV y  bagE γ x Y))%I γ with "[] [] [Hbag]"); eauto.
57 58 59 60 61 62 63 64 65 66 67 68 69
    { 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.