fg_bag.v 9.26 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
(** Concurrent bag specification from the HOCAP paper.
    "Modular Reasoning about Separation of Concurrent Data Structures"
    <http://www.kasv.dk/articles/hocap-ext.pdf>

Fine-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".

Dan Frumin's avatar
Dan Frumin committed
16
(** Fine-grained bag implementation using CAS *)
17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
Definition newBag : val := λ: <>,
  ref NONE.
Definition pushBag : val := rec: "push" "b" "v" :=
  let: "oHead" := !"b" in
  if: CAS "b" "oHead" (SOME (ref ("v", "oHead")))
  then #()
  else "push" "b" "v".

Definition popBag : val := rec: "pop" "b" :=
  match: !"b" with
    NONE => NONE
  | SOME "l" =>
    let: "hd" := !"l" in
    let: "v" := Fst "hd" in
    let: "tl" := Snd "hd" in
    if: CAS "b" (SOME "l") "tl"
    then SOME "v"
    else "pop" "b"
  end.

37
Canonical Structure valmultisetO := leibnizO (gmultiset valO).
38
Class bagG Σ := BagG
39
{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetO));
40 41 42 43 44 45 46 47 48 49 50 51
}.

(** Generic specification for the bag, using view shifts. *)
Section proof.
  Context `{heapG Σ, bagG Σ}.
  Variable N : namespace.

  Definition rown (l : loc) (v : val) :=
    ( q, l {q} v)%I.
  Lemma rown_duplicate l v : rown l v - rown l v  rown l v.
  Proof. iDestruct 1 as (q) "[Hl Hl']". iSplitL "Hl"; iExists _; eauto. Qed.

52 53 54 55
  Definition oloc_to_val (ol: option loc) : val :=
    match ol with
    | None => NONEV
    | Some loc => SOMEV (#loc)
56
    end.
57 58
  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
  Proof. intros [|][|]; simpl; congruence. Qed.
59

60 61 62 63 64 65 66
  Fixpoint is_list (hd : option loc) (xs : list val) : iProp Σ :=
    match xs, hd with
    | [], None => True
    | x::xs, Some l =>  (tl : option loc),
                   rown l (x, oloc_to_val tl)  is_list tl xs
    | _, _ => False
    end%I.
67

68 69 70
  Lemma is_list_duplicate hd xs : is_list hd xs - is_list hd xs  is_list hd xs.
  Proof.
    iInduction xs as [ | x xs ] "IH" forall (hd); simpl; eauto.
71 72
    destruct hd; last by auto.
    iDestruct 1 as (tl) "[Hro Htl]".
73 74
    rewrite rown_duplicate. iDestruct "Hro" as "[Hro Hro']".
    iDestruct ("IH" with "Htl") as "[Htl Htl']".
75
    iSplitL "Hro Htl"; iExists _; iFrame; eauto.
76 77 78 79 80
  Qed.

  Lemma is_list_agree hd xs ys : is_list hd xs - is_list hd ys - xs = ys.
  Proof.
    iInduction xs as [ | x xs ] "IH" forall (hd ys); simpl; eauto.
81 82 83
    - destruct hd; first by auto.
      destruct ys; eauto.
    - destruct hd; last by auto.
84
      destruct ys as [| y ys]; eauto. simpl.
85 86
      iDestruct 1 as (tl) "(Hro & Hls)".
      iDestruct 1 as (tl') "(Hro' & Hls')".
87 88
      iDestruct "Hro" as (q) "Hro".
      iDestruct "Hro'" as (q') "Hro'".
89
      iDestruct (mapsto_agree l q q' (PairV x (oloc_to_val tl)) (PairV y (oloc_to_val tl'))
90 91
                with "Hro Hro'") as %?. simplify_eq/=.
      iDestruct ("IH" with "Hls Hls'") as %->. done.
Ralf Jung's avatar
Ralf Jung committed
92
  Qed.
93 94

  Definition bag_inv (γb : gname) (b : loc) : iProp Σ :=
95 96
    ( (hd : option loc) (ls : list val),
        b  oloc_to_val hd  is_list hd ls  own γb ((1/2)%Qp, to_agree (list_to_set_disj ls)))%I.
97 98 99 100 101 102 103 104 105 106 107 108 109
  Definition is_bag (γb : gname) (x : val) :=
    ( (b : loc), x = #b  inv N (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.
Ralf Jung's avatar
Ralf Jung committed
110
    rewrite /bag_contents. apply bi.wand_intro_r.
111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
    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. iApply wp_fupd.
    wp_alloc r as "Hr".
    iMod (own_alloc (1%Qp, to_agree )) as (γb) "[Ha Hf]"; first done.
    iMod (inv_alloc N _ (bag_inv γb r) with "[Ha Hr]") as "#Hinv".
139
    { iNext. iExists None,[]. simpl. iFrame. }
140 141 142 143 144 145 146
    iModIntro. iApply "HΦ".
    rewrite /is_bag /bag_contents. iFrame.
    iExists _. by iFrame "Hinv".
  Qed.

  Lemma pushBag_spec (P Q : iProp Σ) γ (x v : val)  :
     ( (X : gmultiset val), bag_contents γ X  P
Ralf Jung's avatar
Ralf Jung committed
147
                     ={⊤∖↑N}=  (bag_contents γ ({[v]}  X)  Q)) -
148 149 150 151 152 153 154
    {{{ is_bag γ x  P }}}
      pushBag x (of_val v)
    {{{ RET #(); Q }}}.
  Proof.
    iIntros "#Hvs".
    iIntros (Φ). iAlways. iIntros "[#Hbag HP] HΦ".
    unfold pushBag.
155
    iLöb as "IH". wp_rec. wp_pures.
156 157 158 159 160 161 162
    rewrite /is_bag.
    iDestruct "Hbag" as (b) "[% #Hinv]"; simplify_eq/=.
    wp_bind (! #b)%E.
    iInv N as (o ls) "[Ho [Hls >Hb]]" "Hcl".
    wp_load.
    iMod ("Hcl" with "[Ho Hls Hb]") as "_".
    { iNext. iExists _,_. iFrame. } clear ls.
163
    iModIntro.
164
    wp_alloc n as "Hn".
165
    wp_pures. wp_bind (CAS _ _ _).
166 167
    iInv N as (o' ls) "[Ho [Hls >Hb]]" "Hcl".
    destruct (decide (o = o')) as [->|?].
168
    - wp_cas_suc. { destruct o'; left; done. }
169 170
      iMod ("Hvs" with "[$Hb $HP]") as "[Hb HQ]".
      iMod ("Hcl" with "[Ho Hn Hls Hb]") as "_".
171 172
      { iNext. iExists (Some _),(v::ls). iFrame "Ho Hb".
        simpl. iExists _. iFrame. by iExists 1%Qp. }
173 174
      iModIntro. wp_if_true. by iApply "HΦ".
    - wp_cas_fail.
175 176
      { destruct o, o'; simpl; congruence. }
      { destruct o'; left; done. }
177 178 179 180 181 182 183 184
      iMod ("Hcl" with "[Ho Hls Hb]") as "_".
      { iNext. iExists _,ls. by iFrame "Ho Hb". }
      iModIntro. wp_if_false.
      by iApply ("IH" with "HP [HΦ]").
  Qed.

  Lemma popBag_spec (P : iProp Σ) (Q : val  iProp Σ) γ x :
     ( (X : gmultiset val) (y : val),
Ralf Jung's avatar
Ralf Jung committed
185
               bag_contents γ ({[y]}  X)  P
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201
               ={⊤∖↑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.
    iLöb as "IH". wp_rec.
    rewrite /is_bag.
    iDestruct "Hbag" as (b) "[% #Hinv]"; simplify_eq/=.
    wp_bind (!#b)%E.
    iInv N as (o ls) "[Ho [Hls >Hb]]" "Hcl".
    wp_load.
    destruct ls as [|x ls]; simpl.
202
    - destruct o; first done.
203 204 205 206 207
      iMod ("Hvs2" with "[$Hb $HP]") as "[Hb HQ]".
      iMod ("Hcl" with "[Ho Hb]") as "_".
      { iNext. iExists _,[]. by iFrame. }
      iModIntro. repeat wp_pure _.
      by iApply "HΦ".
208 209
    - destruct o as [hd|]; last done.
      iDestruct "Hls" as (tl) "(Hhd & Hls)"; simplify_eq/=.
210 211 212
      rewrite rown_duplicate. iDestruct "Hhd" as "[Hhd Hhd']".
      rewrite is_list_duplicate. iDestruct "Hls" as "[Hls Hls']".
      iMod ("Hcl" with "[Ho Hb Hhd Hls]") as "_".
213 214
      { iNext. iExists (Some _),(x::ls). simpl; iFrame; eauto.
        iExists _; eauto. by iFrame. }
215 216 217 218 219
      iModIntro. repeat wp_pure _.
      iDestruct "Hhd'" as (q) "Hhd".
      wp_load. repeat wp_pure _.
      wp_bind (CAS _ _ _).
      iInv N as (o' ls') "[Ho [Hls >Hb]]" "Hcl".
220
      destruct (decide (o' = (Some hd))) as [->|?].
221 222 223
      + wp_cas_suc.
        (* The list is still the same *)
        rewrite (is_list_duplicate tl). iDestruct "Hls'" as "[Hls' Htl]".
224 225
        iAssert (is_list (Some hd) (x::ls)) with "[Hhd Hls']" as "Hls'".
        { simpl. iExists tl. iFrame. iExists q. iFrame. }
226 227
        iDestruct (is_list_agree with "Hls Hls'") as %?. simplify_eq.
        iClear "Hls'".
228
        iDestruct "Hls" as (tl') "(Hro' & Htl')".
229 230 231
        iMod ("Hvs1" with "[$Hb $HP]") as "[Hb HQ]".
        iMod ("Hcl" with "[Ho Htl Hb]") as "_".
        { iNext. iExists _,ls. by iFrame "Ho Hb". }
232
        iModIntro. wp_pures. by iApply "HΦ".
233
      + wp_cas_fail. { destruct o'; simpl; congruence. }
234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251
        iMod ("Hcl" with "[Ho Hls Hb]") as "_".
        { iNext. iExists _,ls'. by iFrame "Ho Hb". }
        iModIntro. wp_if_false.
        by iApply ("IH" with "HP [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 |}.