cg_bag.v 6.47 KB
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.
64
  Definition is_bag (γb : gname) (x : val) :=
65 66 67

    ( (lk : val) (b : loc) (γ : gname),
        x = PairV #b lk  is_lock N γ lk (bag_inv γb b))%I.
68
  Definition bag_contents (γb : gname) (X : gmultiset val) : iProp Σ :=
69 70
    own γb ((1/2)%Qp, to_agree X).

71
  Global Instance is_bag_persistent γb x : Persistent (is_bag γb x).
72
  Proof. apply _. Qed.
73
  Global Instance bag_contents_timeless γb X : Timeless (bag_contents γb X).
74 75
  Proof. apply _. Qed.

76 77
  Lemma bag_contents_agree γb X Y :
    bag_contents γb X - bag_contents γb Y - X = Y.
78
  Proof.
79
    rewrite /bag_contents. apply uPred.wand_intro_r.
80 81 82 83 84
    rewrite -own_op own_valid uPred.discrete_valid.
    f_equiv=> /=. rewrite pair_op.
    by intros [_ ?%agree_op_invL'].
  Qed.

85 86
  Lemma bag_contents_update γb X X' Y :
    bag_contents γb X  bag_contents γb X' == bag_contents γb Y  bag_contents γb Y.
87 88
  Proof.
    iIntros "[Hb1 Hb2]".
89
    iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
90 91 92 93 94
    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]".
95
    rewrite /bag_contents. by iFrame.
96 97 98 99 100
  Qed.

  Lemma newBag_spec :
    {{{ True }}}
      newBag #()
101
    {{{ x γ, RET x; is_bag γ x  bag_contents γ  }}}.
102 103 104 105 106 107 108 109 110
  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Φ".
111
    rewrite /is_bag /bag_contents. iFrame.
112 113 114 115 116
    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)  :
117 118 119
     ( (X : gmultiset val), bag_contents γ X  P
                     ={∖↑N}=  (bag_contents γ ({[v]}  X)  Q)) -
    {{{ is_bag γ x  P }}}
120 121 122 123 124 125
      pushBag x (of_val v)
    {{{ RET #(); Q }}}.
  Proof.
    iIntros "#Hvs".
    iIntros (Φ). iAlways. iIntros "[#Hbag HP] HΦ".
    unfold pushBag. do 2 wp_rec.
126
    rewrite /is_bag /bag_inv.
127 128 129 130 131
    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.
132 133
    wp_bind (_ <- _)%E.
    iApply (wp_mask_mono _ (∖↑N)); first done.
134
    iMod ("Hvs" with "[$Ha $HP]") as "[Hbc HQ]".
135
    wp_store. wp_let.
136 137 138 139 140 141 142
    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),
143 144 145 146
               bag_contents γ ({[y]}  X)  P
               ={∖↑N}=  (bag_contents γ X  Q (SOMEV y))) -
     (bag_contents γ   P ={∖↑N}=  (bag_contents γ   Q NONEV)) -
    {{{ is_bag γ x  P }}}
147 148 149 150 151 152
      popBag x
    {{{ v, RET v; Q v }}}.
  Proof.
    iIntros "#Hvs1 #Hvs2".
    iIntros (Φ). iAlways. iIntros "[#Hbag HP] HΦ".
    unfold popBag. wp_rec.
153
    rewrite /is_bag /bag_inv.
154 155 156 157
    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]".
158 159 160
    wp_seq. wp_bind (!#b)%E.
    iApply (wp_mask_mono _ (∖↑N)); first done.
    destruct ls as [|v ls]; simpl.
161
    - iMod ("Hvs2" with "[$Ha $HP]") as "[Hbc HQ]".
162
      wp_load. repeat wp_pure _.
163 164 165 166
      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]".
167
      wp_load. repeat wp_pure _. wp_store. do 2 wp_pure _.
168 169 170 171 172 173 174
      wp_apply (release_spec with  "[$Hlk $Htok Hbc Hb]").
      { iExists ls; iFrame. }
      iIntros "_". repeat wp_pure _. by iApply "HΦ".
  Qed.

End proof.

175
Typeclasses Opaque bag_contents is_bag.
176 177

Canonical Structure cg_bag `{!heapG Σ, !bagG Σ} : bag Σ :=
178 179 180 181 182
  {| 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;
183 184 185 186
     abstract_bag.newBag_spec := newBag_spec;
     abstract_bag.pushBag_spec := pushBag_spec;
     abstract_bag.popBag_spec := popBag_spec |}.