abstract_bag.v 2.17 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
(** 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 locked with is_lock *)
  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
34
                     ={∖↑N}=  (bag_contents γ ({[v]}  X)  Q)) -
35 36 37 38 39 40
    {{{ 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
41 42
               ={∖↑N}=  (bag_contents γ X  Q (SOMEV y))) -
     (bag_contents γ   P ={∖↑N}=  (bag_contents γ   Q NONEV)) -
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
    {{{ 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.