Commit a1c9f69a authored by Dan Frumin's avatar Dan Frumin

Update comments

parent bc082bf8
...@@ -15,7 +15,7 @@ Structure bag Σ `{!heapG Σ} := Bag { ...@@ -15,7 +15,7 @@ Structure bag Σ `{!heapG Σ} := Bag {
pushBag : val; pushBag : val;
popBag : val; popBag : val;
(* -- predicates -- *) (* -- predicates -- *)
(* name is used to associate locked with is_lock *) (* name is used to associate bag_contents with is_bag *)
name : Type; name : Type;
is_bag (N: namespace) (γ: name) (b: val) : iProp Σ; is_bag (N: namespace) (γ: name) (b: val) : iProp Σ;
bag_contents (γ: name) (X: gmultiset val) : iProp Σ; bag_contents (γ: name) (X: gmultiset val) : iProp Σ;
......
...@@ -16,6 +16,7 @@ Section proof. ...@@ -16,6 +16,7 @@ Section proof.
Variable b : bag Σ. Variable b : bag Σ.
Variable N : namespace. 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 Σ := Definition bagE (γ : name Σ b) (x : val) (X : gmultiset val) : iProp Σ :=
(is_bag b N γ x bag_contents b γ X)%I. (is_bag b N γ x bag_contents b γ X)%I.
......
...@@ -13,7 +13,7 @@ From iris.heap_lang.lib Require Import lock spin_lock. ...@@ -13,7 +13,7 @@ From iris.heap_lang.lib Require Import lock spin_lock.
From iris_examples.hocap Require Import abstract_bag. From iris_examples.hocap Require Import abstract_bag.
Set Default Proof Using "Type". Set Default Proof Using "Type".
(** Coarse-grained bag implementation using a spin lock *) (** Fine-grained bag implementation using CAS *)
Definition newBag : val := λ: <>, Definition newBag : val := λ: <>,
ref NONE. ref NONE.
Definition pushBag : val := rec: "push" "b" "v" := Definition pushBag : val := rec: "push" "b" "v" :=
......
...@@ -17,7 +17,9 @@ Section proof. ...@@ -17,7 +17,9 @@ Section proof.
Variable N : namespace. Variable N : namespace.
Definition NB := N.@"bag". Definition NB := N.@"bag".
Definition NI := N.@"inv". Definition NI := N.@"inv".
Variable P : val val iProp Σ. (* Predicate that will be satisfied by all the elements in the bag *) (** Predicate that will be satisfied by all the elements in the bag.
The first argument is the bag itself. *)
Variable P : val val iProp Σ.
Definition bagS_inv (γ : name Σ b) (y : val) : iProp Σ := Definition bagS_inv (γ : name Σ b) (y : val) : iProp Σ :=
inv NI ( X, bag_contents b γ X [ mset] x X, P y x)%I. inv NI ( X, bag_contents b γ X [ mset] x X, P y x)%I.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment