merge with original repo

_CoqProject

@@ -110,3 +110,5 @@ theories/logatom/conditional_increment/cinc.v
 theories/logatom/rdcss/rdcss.v
 theories/logatom/rdcss/spec.v
 theories/logatom/proph_erasure.v
+theories/logatom/herlihy_wing_queue/spec.v
+theories/logatom/herlihy_wing_queue/hwq.v

opam

 opam-version: "1.2"
 name: "coq-iris-examples"
 maintainer: "Ralf Jung <jung@mpi-sws.org>"
-authors: "The Iris Team"
+authors: "The Iris Team and Contributors"
 homepage: "http://iris-project.org/"
 bug-reports: "https://gitlab.mpi-sws.org/FP/iris-examples/issues"
 dev-repo: "https://gitlab.mpi-sws.org/FP/iris-examples.git"
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2019-07-01.1.6e79f000") | (= "dev") }
+  "coq-iris" { (= "dev.2019-07-05.0.d392b7a6") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]

theories/logatom/herlihy_wing_queue/spec.v

+From iris.heap_lang Require Export lifting notation.
+From iris.program_logic Require Export atomic.
+Set Default Proof Using "Type".
+
+(** A general logically atomic interface for Herlihy-Wing queues. *)
+Record atomic_hwq {Σ} `{!heapG Σ} := AtomicHWQ {
+  (* -- operations -- *)
+  new_queue : val;
+  enqueue : val;
+  dequeue : val;
+  (* -- other data -- *)
+  name : Type;
+  name_eqdec : EqDecision name;
+  name_countable : Countable name;
+  (* -- predicates -- *)
+  is_hwq (N : namespace) (sz : nat) (γ : name) (v : val) : iProp Σ;
+  hwq_content (γ : name) (ls : list loc) : iProp Σ;
+  (* -- predicate properties -- *)
+  is_hwq_persistent N sz γ v : Persistent (is_hwq N sz γ v);
+  hwq_content_timeless γ ls : Timeless (hwq_content γ ls);
+  hwq_content_exclusive γ ls1 ls2 :
+    hwq_content γ ls1 -∗ hwq_content γ ls2 -∗ False;
+  (* -- operation specs -- *)
+  new_queue_spec N (sz : nat) :
+    0 < sz →
+    {{{ True }}}
+      new_queue #sz
+    {{{ v γ, RET v; is_hwq N sz γ v ∗ hwq_content γ [] }}};
+  enqueue_spec N (sz : nat) (γ : name) (q : val) (l : loc) :
+    is_hwq N sz γ q -∗
+    <<< ∀ (ls : list loc), hwq_content γ ls >>>
+      enqueue q #l @ ⊤ ∖ ↑N
+    <<< hwq_content γ (ls ++ [l]), RET #() >>>;
+  dequeue_spec N (sz : nat) (γ : name) (q : val) :
+    is_hwq N sz γ q -∗
+    <<< ∀ (ls : list loc), hwq_content γ ls >>>
+      dequeue q @ ⊤ ∖ ↑N
+    <<< ∃ (l : loc) ls', ⌜ls = l :: ls'⌝ ∗ hwq_content γ ls', RET #l >>>;
+}.
+Arguments atomic_hwq _ {_}.
+
+Existing Instances is_hwq_persistent hwq_content_timeless.

theories/logatom/snapshot/atomic_snapshot.v

@@ -13,7 +13,7 @@ Set Default Proof Using "Type".
 
 
 (*
-     newPair v :=
+     new_snapshot v :=
        ref (ref (v, 0))
  *)
 Definition new_snapshot : val :=
@@ -56,10 +56,10 @@ Definition read : val :=
       let (_, v') = !!xp in
       if v = v'
         then (x, y)
-        else readPair l
+        else read_with l
  *)
 Definition read_with_proph : val :=
-  rec: "readPair" "xp" "l" :=
+  rec: "read_with" "xp" "l" :=
     let: "proph"  := NewProph in
     let: "x"  := ! !"xp" in
     let: "y"  := !"l" in
@@ -68,7 +68,7 @@ Definition read_with_proph : val :=
     resolve_proph: "proph" to: "v_eq" ;;
     if: "v_eq"
     then (Fst "x", "y")
-    else  "readPair" "xp" "l".
+    else  "read_with" "xp" "l".
 
 
 (** The CMRA & functor we need. *)