cg_bag.v 6.52 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
(** 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 := λ: <>,
Robbert Krebbers's avatar
Robbert Krebbers committed
18 19 20
  let: "r" := ref NONE in
  let: "l" := newlock #() in
  ("r", "l").
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40
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".

Robbert Krebbers's avatar
Robbert Krebbers committed
41
Canonical Structure valmultisetO := leibnizO (gmultiset valO).
42
Class bagG Σ := BagG
Robbert Krebbers's avatar
Robbert Krebbers committed
43
{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetO));
44 45 46 47 48 49 50 51 52 53 54
  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 => 
Ralf Jung's avatar
Ralf Jung committed
55
    | SOMEV (v1, t) => {[v1]}  bag_of_val t
56 57 58 59 60 61 62 63 64
    | _ => 
    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 Σ :=
Ralf Jung's avatar
Ralf Jung committed
65
    ( ls : list val, b  (val_of_list ls)  own γb ((1/2)%Qp, to_agree (list_to_set_disj ls)))%I.
66
  Definition is_bag (γb : gname) (x : val) :=
67 68 69

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

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

78 79
  Lemma bag_contents_agree γb X Y :
    bag_contents γb X - bag_contents γb Y - X = Y.
80
  Proof.
Ralf Jung's avatar
Ralf Jung committed
81
    rewrite /bag_contents. apply bi.wand_intro_r.
82
    rewrite -own_op own_valid uPred.discrete_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
    f_equiv=> /=. rewrite -pair_op.
84 85 86
    by intros [_ ?%agree_op_invL'].
  Qed.

87 88
  Lemma bag_contents_update γb X X' Y :
    bag_contents γb X  bag_contents γb X' == bag_contents γb Y  bag_contents γb Y.
89 90
  Proof.
    iIntros "[Hb1 Hb2]".
91
    iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
92
    iMod (own_update_2 with "Hb1 Hb2") as "Hb".
Robbert Krebbers's avatar
Robbert Krebbers committed
93
    { rewrite -pair_op frac_op'.
94 95 96
      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]".
97
    rewrite /bag_contents. by iFrame.
98 99 100 101 102
  Qed.

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

End proof.

176
Typeclasses Opaque bag_contents is_bag.
177 178

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