add a client to the atomic increment

theories/heap_lang/lib/atomic_heap.v

@@ -24,21 +24,21 @@ Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
     atomic_wp (load #l)%E
               (λ '(v, q), mapsto l q v)
               (λ '(v, q) (_:()), mapsto l q v)
-              ⊤ ∅
+              ⊤ ⊤
               (λ '(v, q) _, v);
   store_spec (l : loc) (e : expr) (w : val) :
     IntoVal e w →
     atomic_wp (store (#l, e))%E
               (λ v, mapsto l 1 v)
               (λ v (_:()), mapsto l 1 w)
-              ⊤ ∅
+              ⊤ ⊤
               (λ _ _, #()%V);
   cas_spec (l : loc) (e1 e2 : expr) (w1 w2 : val) :
     IntoVal e1 w1 → IntoVal e2 w2 →
     atomic_wp (cas (#l, e1, e2))%E
               (λ v, mapsto l 1 v)
               (λ v (_:()), if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v)
-              ⊤ ∅
+              ⊤ ⊤
               (λ v _, #(if decide (v = w1) then true else false)%V);
 }.
 Arguments atomic_heap _ {_}.
@@ -66,7 +66,7 @@ Section proof.
     atomic_wp (primitive_load #l)%E
               (λ '(v, q), l ↦{q} v)%I
               (λ '(v, q) (_:()), l ↦{q} v)%I
-              ⊤ ∅
+              ⊤ ⊤
               (λ '(v, q) _, v).
   Proof.
     iIntros (Φ) "Aupd". wp_let.
@@ -79,7 +79,7 @@ Section proof.
     atomic_wp (primitive_store (#l, e))%E
               (λ v, l ↦ v)%I
               (λ v (_:()), l ↦ w)%I
-              ⊤ ∅
+              ⊤ ⊤
               (λ _ _, #()%V).
   Proof.
     iIntros (<-%of_to_val Φ) "Aupd". wp_let. wp_proj. wp_proj.
@@ -92,7 +92,7 @@ Section proof.
     atomic_wp (primitive_cas (#l, e1, e2))%E
               (λ v, l ↦ v)%I
               (λ v (_:()), if decide (v = w1) then l ↦ w2 else l ↦ v)%I
-              ⊤ ∅
+              ⊤ ⊤
               (λ v _, #(if decide (v = w1) then true else false)%V).
   Proof.
     iIntros (<-%of_to_val <-%of_to_val Φ) "Aupd". wp_let. repeat wp_proj.

theories/heap_lang/lib/increment.v

@@ -2,7 +2,7 @@ From iris.heap_lang Require Export lifting notation.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation atomic_heap.
+From iris.heap_lang Require Import proofmode notation atomic_heap par.
 Set Default Proof Using "Type".
 
 (** Show taht implementing fetch-and-add on top of CAS preserves logical
@@ -10,7 +10,7 @@ atomicity. *)
 
 (* TODO: Move this to iris-examples once gen_proofmode is merged. *)
 Section increment.
-  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
+  Context `{!heapG Σ} (aheap: atomic_heap Σ).
 
   Definition incr: val :=
     rec: "incr" "l" :=
@@ -23,7 +23,7 @@ Section increment.
         atomic_wp (incr #l)
                   (λ (v: Z), aheap.(mapsto) l 1 #v)%I
                   (λ v (_:()), aheap.(mapsto) l 1 #(v + 1))%I
-                  ⊤ ∅
+                  ⊤ ⊤
                   (λ v _, #v).
   Proof.
     iIntros (Φ) "AUpd". iLöb as "IH". wp_let.
@@ -56,3 +56,40 @@ Section increment.
 
 End increment.
 
+Section increment_client.
+  Context `{!heapG Σ, !spawnG Σ}.
+
+  Definition incr_client : val :=
+    λ: "x",
+       let: "l" := ref "x" in
+       incr primitive_atomic_heap "l" ||| incr primitive_atomic_heap "l".
+
+  Lemma incr_client_safe (x: Z):
+    WP incr_client #x {{ _, True }}%I.
+  Proof using Type*.
+    wp_let. wp_alloc l as "Hl". wp_let.
+    iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
+    (* FIXME: I am only usign persistent stuff, so I should be allowed
+       to move this to the persisten context even without the additional □. *)
+    iAssert (□ atomic_update (λ (v: Z), l ↦ #v)
+                           (λ v (_:()), l ↦ #(v + 1))
+                           ⊤ ⊤
+                           (λ _ _, True))%I as "#Aupd".
+    { iAlways. iExists True%I, True%I. repeat (iSplit; first done). clear x.
+      iIntros (E) "!# % _".
+      assert (E = ⊤) as -> by set_solver.
+      iInv nroot as (x) ">H↦" "Hclose".
+      iMod fupd_intro_mask' as "Hclose2"; last iModIntro; first set_solver.
+      iExists _. iFrame. iSplit.
+      { iIntros "H↦". iMod "Hclose2" as "_". iMod ("Hclose" with "[-]"); last done.
+        iNext. iExists _. iFrame. }
+      iIntros (_) "H↦". iMod "Hclose2" as "_".
+      iMod ("Hclose" with "[-]"); last done. iNext. iExists _. iFrame. }
+    wp_apply (wp_par (λ _, True)%I (λ _, True)%I).
+    - wp_apply incr_spec. iAssumption. (* FIXME: without giving the
+      postconditions above, this diverges. *)
+    - wp_apply incr_spec. iAssumption.
+    - iIntros (??) "_ !>". done.
+  Qed.
+
+End increment_client.