Merge branch 'hocap' into 'master'

Implement modular specifications from the HOCAP paper

See merge request FP/iris-examples!5

README.md

@@ -57,6 +57,7 @@ This repository contains the following case studies:
   [report](http://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf).
 * [lecture-notes](theories/lecture_notes): Coq examples for the
   [Iris lecture notes](http://iris-project.org/tutorial-material.html).
+* [hocap](theories/hocap): Formalisations of the concurrent bag and concurrent runners libraries from the [HOCAP paper](https://dl.acm.org/citation.cfm?id=2450283). See the associated [README](theories/hocap/README.md).
 
 ## For Developers: How to update the Iris dependency
 

_CoqProject

@@ -70,3 +70,13 @@ theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
 theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
 theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
 theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
+
+theories/hocap/abstract_bag.v
+theories/hocap/cg_bag.v
+theories/hocap/fg_bag.v
+theories/hocap/exclusive_bag.v
+theories/hocap/shared_bag.v
+theories/hocap/contrib_bag.v
+theories/hocap/lib/oneshot.v
+theories/hocap/concurrent_runners.v
+theories/hocap/parfib.v

theories/hocap/README.md

+These examples are meant to demonstrate the applicability in Iris of the specification style for concurrent data structures described in the paper
+[Modular reasoning about separation of concurrent data structures](https://link.springer.com/chapter/10.1007/978-3-642-37036-6_11).
+
+## Overview
+
+* [abstract_bag](abstract_bag.v) describes the generic abstract bag specification (Section 1);
+* in [exclusive_bag](exclusive_bag.v) and [shared_bag](shared_bag.v) the exclusive/sequential and shared/concurrent specifications are derived from the generic abstract specification (Section 3);
+* [cg_bag.v](cg_bag.v) and [fg_bag](fg_bag.v) provide two implementations for the abstract bag specification (Section 3);
+* [concurrent_runners](concurrent_runners.v) implements the (impredicative) concurrent runner specification from Section 4;
+* [parfib](parfib.v) demonstrates the usage of the concurrent runners library (Section 4).
+* [contrib_bag.v](contrib_bag.v) -- bag specification "with contributions" a-la counter with contributions, allows for multiple concurrent `push` operations and a sequential `pop` operation.
+
+## Differences with the paper proofs
+
+### Circularity in `concurrent_runners`
+
+There is a circularity in the proof of `newRunner`, which is perhaps more poignant in ML/Heap-lang than in C#.
+
+On the first line of `newRunner`, one creates a bag and has to pick a predicate that should hold for every element in the bag.
+However, the predicate that we want to have refers to the runner itself -- which is a pair of a `bag` and a `body`.
+In this setting, the runner is not yet available at this point in time.
+There are (at least) two potential ways of resolving this circularity:
+
+1. Allow the `P` predicate in the `shared_bag` specification to refer to the bag itself (as a formal parameter);
+2. Have a specification that would construct a bag in several steps: the `newBag_spec` will return a token that can be view-shifted later at an arbitrary point in time to `bagS b P` -- this will allow the client to pick `P` at a more comfortable point.
+
+We chose to go with option 1 in this formalisation.

theories/hocap/abstract_bag.v

+(** Concurrent bag specification from the HOCAP paper.
+    "Modular Reasoning about Separation of Concurrent Data Structures"
+    <http://www.kasv.dk/articles/hocap-ext.pdf>
+
+This file: abstract bag specification
+*)
+From iris.heap_lang Require Export lifting notation.
+From iris.base_logic.lib Require Export invariants.
+From stdpp Require Import gmultiset.
+Set Default Proof Using "Type".
+
+Structure bag Σ `{!heapG Σ} := Bag {
+  (* -- operations -- *)
+  newBag : val;
+  pushBag : val;
+  popBag : val;
+  (* -- predicates -- *)
+  (* name is used to associate bag_contents with is_bag *)
+  name : Type;
+  is_bag (N: namespace) (γ: name) (b: val) : iProp Σ;
+  bag_contents (γ: name) (X: gmultiset val) : iProp Σ;
+  (* -- ghost state theory -- *)
+  is_bag_persistent N γ b : Persistent (is_bag N γ b);
+  bag_contents_timeless γ X : Timeless (bag_contents γ X);
+  bag_contents_agree γ X Y: bag_contents γ X -∗ bag_contents γ Y -∗ ⌜X = Y⌝;
+  bag_contents_update γ X X' Y:
+    bag_contents γ X ∗ bag_contents γ X' ==∗
+    bag_contents γ Y ∗ bag_contents γ Y;
+  (* -- operation specs -- *)
+  newBag_spec N :
+    {{{ True }}} newBag #() {{{ x γ, RET x; is_bag N γ x ∗ bag_contents γ ∅ }}};
+  pushBag_spec N P Q γ b v :
+    □ (∀ (X : gmultiset val), bag_contents γ X ∗ P
+                     ={⊤∖↑N}=∗ ▷ (bag_contents γ ({[v]} ∪ X) ∗ Q)) -∗
+    {{{ is_bag N γ b ∗ P }}}
+      pushBag b (of_val v)
+    {{{ RET #(); Q }}};
+  popBag_spec N P Q γ b :
+    □ (∀ (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 N γ b ∗ P }}}
+      popBag b
+    {{{ v, RET v; Q v }}};
+}.
+
+Arguments newBag {_ _} _.
+Arguments popBag {_ _} _.
+Arguments pushBag {_ _} _.
+Arguments newBag_spec {_ _} _ _ _.
+Arguments popBag_spec {_ _} _ _ _ _ _ _.
+Arguments pushBag_spec {_ _} _ _ _ _ _ _ _.
+Arguments is_bag {_ _} _ _ _ _.
+Arguments bag_contents {_ _} _ _.
+Arguments bag_contents_update {_ _} _ {_ _ _}.
+Existing Instances is_bag_persistent bag_contents_timeless.
+

theories/hocap/cg_bag.v

+(** 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).
+  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.
+    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]".
+    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.
+    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.
+    rewrite /is_bag /bag_inv.
+    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_store. wp_let.
+    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.
+    rewrite /is_bag /bag_inv.
+    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_load. repeat wp_pure _.
+      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 |}.
+

theories/hocap/contrib_bag.v

+(** Bag with contributions specification *)
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang proofmode notation.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import gmultiset frac_auth.
+From iris_examples.hocap Require Import abstract_bag.
+Set Default Proof Using "Type".
+
+Section proof.
+  Context `{heapG Σ}.
+  Variable b : bag Σ.
+  Variable N : namespace.
+  Definition NB := N.@"bag".
+  Definition NI := N.@"inv".
+
+  Context `{inG Σ (frac_authR (gmultisetUR val))}.
+
+  Definition bagM_inv (γb : name Σ b) (γ : gname) : iProp Σ :=
+    inv NI (∃ X, bag_contents b γb X ∗ own γ (●! X))%I.
+  Definition bagM (γb : name Σ b) (γ : gname) (x : val) : iProp Σ :=
+    (is_bag b NB γb x ∗ bagM_inv γb γ)%I.
+  Definition bagPart (γ : gname) (q : Qp) (X : gmultiset val) : iProp Σ :=
+    (own γ (◯!{q} X))%I.
+
+  Lemma bagPart_compose (γ: gname) (q1 q2: Qp) (X Y : gmultiset val) :
+    bagPart γ q1 X -∗ bagPart γ q2 Y -∗ bagPart γ (q1+q2) (X ∪ Y).
+  Proof.
+    iIntros "Hp1 Hp2".
+    rewrite /bagPart -gmultiset_op_union -frac_op'.
+    rewrite frag_auth_op own_op. iFrame.
+  Qed.
+  Lemma bagPart_decompose (γ: gname) (q: Qp) (X Y : gmultiset val) :
+    bagPart γ q (X ∪ Y) -∗ bagPart γ (q/2) X ∗ bagPart γ (q/2) Y.
+  Proof.
+    iIntros "Hp".
+    assert (q = (q/2)+(q/2))%Qp as Hq by (by rewrite Qp_div_2).
+    rewrite /bagPart {1}Hq.
+    rewrite -gmultiset_op_union -frac_op'.
+    rewrite frag_auth_op own_op. iFrame.
+  Qed.
+
+  Global Instance bagM_persistent γb γ x : Persistent (bagM γb γ x).
+  Proof. apply _. Qed.
+
+  Lemma newBag_spec :
+    {{{ True }}}
+      newBag b #()
+    {{{ x, RET x; ∃ γb γ, bagM γb γ x ∗ bagPart γ 1 ∅ }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ". iApply wp_fupd.
+    iApply (newBag_spec b NB); eauto.
+    iNext. iIntros (v γb) "[#Hbag Hcntn]".
+    iMod (own_alloc (●! ∅ ⋅ ◯! ∅)) as (γ) "[Hown Hpart]"; first done.
+    iMod (inv_alloc NI _ (∃ X, bag_contents b γb X ∗ own γ (●! X))%I with "[Hcntn Hown]") as "#Hinv".
+    { iNext. iExists _. iFrame. }
+    iApply "HΦ". iModIntro. iExists _,_. iFrame "Hinv Hbag Hpart".
+  Qed.
+
+  Lemma pushBag_spec γb γ x v q Y :
+    {{{ bagM γb γ x ∗ bagPart γ q Y }}}
+       pushBag b x (of_val v)
+    {{{ RET #(); bagPart γ q ({[v]} ∪ Y) }}}.
+  Proof.
+    iIntros (Φ) "[#[Hbag Hinv] HP] HΦ". rewrite /bagM_inv.
+    iApply (pushBag_spec b NB (bagPart γ q Y)%I (bagPart γ q ({[v]} ∪ Y))%I with "[] [Hbag HP]"); eauto.
+    iAlways. iIntros (X) "[Hb1 HP]".
+    iInv NI as (X') "[>Hb2 >Hown]" "Hcl".
+    iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
+    iMod (bag_contents_update b ({[v]} ∪ X) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
+    rewrite /bagPart.
+    iMod (own_update_2 with "Hown HP") as "[Hown HP]".
+    { apply (frac_auth_update _ _ _ ({[v]} ∪ X) ({[v]} ∪ Y)).
+      do 2 rewrite (comm _ {[v]}).
+      apply gmultiset_local_update_alloc. }
+    iFrame. iApply "Hcl".
+    iNext. iExists _; iFrame.
+  Qed.
+
+  Local Ltac multiset_solver :=
+    intro;
+    repeat (rewrite multiplicity_difference || rewrite multiplicity_union);
+    (omega || naive_solver).
+
+  Lemma popBag_spec γb γ x X :
+    {{{ bagM γb γ x ∗ bagPart γ 1 X }}}
+       popBag b x
+    {{{ v, RET v;
+        (⌜v = NONEV⌝ ∧ ⌜X = ∅⌝ ∗ bagPart γ 1 X)
+       ∨ (∃ y, ⌜v = SOMEV y⌝ ∧ ⌜y ∈ X⌝ ∗ bagPart γ 1 (X ∖ {[y]})) }}}.
+  Proof.
+    iIntros (Φ) "[[#Hbag #Hinv] Hpart] HΦ".
+    iApply (popBag_spec b NB (bagPart γ 1 X)%I
+             (fun v => (⌜v = NONEV⌝ ∧ ⌜X = ∅⌝ ∗ bagPart γ 1 X)
+                     ∨ (∃ y, ⌜v = SOMEV y⌝ ∧ ⌜y ∈ X⌝ ∗ bagPart γ 1 (X ∖ {[y]})))%I with "[] [] [Hpart]"); eauto.
+    { iAlways. iIntros (Y y) "[Hb1 Hpart]".
+      iInv NI as (X') "[>Hb2 >HPs]" "Hcl".
+      iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
+      iMod (bag_contents_update b Y with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
+      rewrite /bagPart.
+      iAssert (⌜X = ({[y]} ∪ Y)⌝)%I with "[Hpart HPs]" as %->.
+      { iDestruct (own_valid_2 with "HPs Hpart") as %Hfoo.
+        apply frac_auth_agree in Hfoo. by unfold_leibniz. }
+      iMod (own_update_2 with "HPs Hpart") as "Hown".
+      { apply (frac_auth_update _ _ _ (({[y]} ∪ Y) ∖ {[y]}) (({[y]} ∪ Y) ∖ {[y]})).
+        apply gmultiset_local_update_dealloc; multiset_solver. }
+      iDestruct "Hown" as "[HPs Hpart]".
+      iMod ("Hcl" with "[-Hpart Hb1]") as "_".
+      { iNext. iExists _; iFrame.
+        assert (Y = (({[y]} ∪ Y) ∖ {[y]})) as <-
+          by (unfold_leibniz; multiset_solver).
+        iFrame. }
+      iModIntro. iNext. iFrame. iRight. iExists y; repeat iSplit; eauto.
+      iPureIntro. by apply elem_of_union_l, elem_of_singleton. }
+    { iAlways. iIntros "[Hb1 Hpart]".
+      iInv NI as (X') "[>Hb2 >HPs]" "Hcl".
+      iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
+      iAssert (⌜X = ∅⌝)%I with "[Hpart HPs]" as %->.
+      { rewrite /bagPart.
+        iDestruct (own_valid_2 with "HPs Hpart") as %Hfoo.
+        apply frac_auth_agree in Hfoo. by unfold_leibniz. }
+      iMod ("Hcl" with "[Hb2 HPs]") as "_".
+      { iNext. iExists _; iFrame. }
+      iModIntro. iNext. iFrame. iLeft; eauto. }
+  Qed.
+
+End proof.

theories/hocap/exclusive_bag.v

+(** 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.
+
+  (** An exclusive specification keeps track of the exact contents of the bag *)
+  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)
+    {{{ RET #(); bagE γ x ({[v]} ∪ X) }}}.
+  Proof.
+    iIntros (Φ) "Hbag HΦ".
+    iApply (pushBag_spec b N (bagE γ x X)%I (bagE γ x ({[v]} ∪ X))%I with "[] [Hbag]"); eauto.
+    { iAlways. iIntros (Y) "[Hb1 Hb2]".
+      iDestruct "Hb2" as "[#Hbag Hb2]".
+      iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
+      iMod (bag_contents_update b ({[v]} ∪ Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
+      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 ∅)
+                 ∨ (∃ Y y, ⌜X = {[y]} ∪ Y⌝ ∧ ⌜v = SOMEV y⌝ ∧ bagE γ x Y)}}}.
+  Proof.
+    iIntros (Φ) "Hbag HΦ".
+    iApply (popBag_spec b N (bagE γ x X)%I (fun v => (⌜X = ∅⌝ ∧ ⌜v = NONEV⌝ ∧ bagE γ x ∅)
+                 ∨ (∃ Y y, ⌜X = {[y]} ∪ Y⌝ ∧ ⌜v = SOMEV y⌝ ∧ bagE γ x Y))%I γ with "[] [] [Hbag]"); eauto.
+    { 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.
+

theories/hocap/fg_bag.v

+(** 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".
+
+(** Fine-grained bag implementation using CAS *)
+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.
+
+Canonical Structure valmultisetC := leibnizC (gmultiset valC).
+Class bagG Σ := BagG
+{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetC));
+}.
+
+(** 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.
+
+  Fixpoint is_list (hd : val) (xs : list val) : iProp Σ :=
+    match xs with
+    | [] => ⌜hd = NONEV⌝%I
+    | x::xs => (∃ (l : loc) (tl : val),
+                   ⌜hd = SOMEV #l⌝ ∗ rown l (x, tl) ∗ is_list tl xs)%I
+    end.
+
+  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.
+    iDestruct 1 as (l tl) "[% [Hro Htl]]"; simplify_eq.
+    rewrite rown_duplicate. iDestruct "Hro" as "[Hro Hro']".
+    iDestruct ("IH" with "Htl") as "[Htl Htl']".
+    iSplitL "Hro Htl"; iExists _,_; iFrame; eauto.
+  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.
+    - iIntros "%"; subst.
+      destruct ys; eauto. simpl.
+      iDestruct 1 as (? ?) "[% ?]". simplify_eq.
+    - iDestruct 1 as (l tl) "(% & Hro & Hls)"; simplify_eq.
+      destruct ys as [| y ys]; eauto. simpl.
+      iDestruct 1 as (l' tl') "(% & Hro' & Hls')"; simplify_eq.
+      iDestruct "Hro" as (q) "Hro".
+      iDestruct "Hro'" as (q') "Hro'".
+      iDestruct (mapsto_agree l' q q' (PairV x tl) (PairV y tl')
+                with "Hro Hro'") as %?. simplify_eq/=.
+      iDestruct ("IH" with "Hls Hls'") as %->. done.
+                                                                             Qed.
+
+  Definition bag_inv (γb : gname) (b : loc) : iProp Σ :=
+    (∃ (hd : val) (ls : list val),
+        b ↦ hd ∗ is_list hd ls ∗ own γb ((1/2)%Qp, to_agree (of_list ls)))%I.
+  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.
+    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.
+