add count with backup case study

README.md

@@ -66,6 +66,9 @@ This repository contains the following case studies:
   - Treiber Stack (by Zhen Zhang, and another version by Rodolphe Lepigre).
   - Flat Combiner (by Zhen Zhang, also see
     [this archived documentation](https://gitlab.mpi-sws.org/FP/iris-atomic/tree/master/docs)).
+  - Counter with a backup, the case study from Section 4 of the
+    [later credits paper](https://plv.mpi-sws.org/later-credits/) (by Simon
+    Spies).
 * [spanning_tree](theories/spanning_tree): Proof of a concurrent spanning tree
   algorithm (by Amin Timany).
 * [concurrent_stacks](theories/concurrent_stacks): Proof of an implementation of

_CoqProject

@@ -96,6 +96,8 @@ theories/logatom/rdcss/rdcss.v
 theories/logatom/rdcss/spec.v
 theories/logatom/herlihy_wing_queue/spec.v
 theories/logatom/herlihy_wing_queue/hwq.v
+theories/logatom/counter_with_backup/counter_spec.v
+theories/logatom/counter_with_backup/counter_proof.v
 
 theories/proph/lib/one_shot_proph.v
 theories/proph/lib/typed_proph.v

coq-iris-examples.opam

@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2022-08-12.4.9245c4c0") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2022-08-14.0.25e3b14e") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 

theories/logatom/counter_with_backup/counter_spec.v

+From iris.program_logic Require Import atomic.
+From iris.heap_lang Require Import proofmode notation.
+From iris.prelude Require Import options.
+
+(** * A general logically atomic interface for an atomic counter. *)
+Record atomic_counter {Σ} `{!heapGS Σ} := AtomicCounter {
+  (* -- operations -- *)
+  new_counter : val;
+  increment : val;
+  get : val;
+  get_backup : val;
+  (* -- other data -- *)
+  name : Type;
+  name_eqdec : EqDecision name;
+  name_countable : Countable name;
+  (* -- predicates -- *)
+  is_counter (N : namespace) (γs : name) (v : val) : iProp Σ;
+  value (γs : name) (n : nat) : iProp Σ;
+  (* -- predicate properties -- *)
+  is_counter_persistent N γs c : Persistent (is_counter N γs c);
+  value_timeless γs n : Timeless (value γs n);
+  value_exclusive γs n1 n2 :
+    value γs n1 -∗ value γs n2 -∗ False;
+  (* -- operation specs -- *)
+  new_counter_spec N :
+    {{{ True }}} new_counter #() {{{ c γs, RET c; is_counter N γs c ∗ value γs 0 }}};
+  (* the following specs are logically atomic, using logically-atomic triples <<< x. P >>> e <<< y. Q >>> *)
+  (* note that the [RET] clause _specifies_ that the return value is [n], and hence we do not need to introduce a separate binder [m] as is done in the formulation shown in the paper *)
+  increment_spec N γs c :
+    is_counter N γs c -∗
+    <<< ∀∀ n: nat, value γs n >>>
+      increment c @ ↑N
+    <<< value γs (n + 1), RET #n >>>;
+  get_spec N γs c :
+    is_counter N γs c -∗
+    <<< ∀∀ n: nat, value γs n >>>
+      get c @ ↑N
+    <<< value γs n, RET #n >>>;
+  get_backup_spec N γs c :
+    is_counter N γs c -∗
+    <<< ∀∀ n: nat, value γs n >>>
+      get_backup c @ ↑N
+    <<< value γs n, RET #n >>>;
+}.
+Global Arguments atomic_counter _ {_}.