add atomic concurrent increment

_CoqProject

@@ -78,6 +78,9 @@ theories/heap_lang/lang.v
 theories/heap_lang/tactics.v
 theories/heap_lang/lifting.v
 theories/heap_lang/notation.v
+theories/heap_lang/proofmode.v
+theories/heap_lang/adequacy.v
+theories/heap_lang/total_adequacy.v
 theories/heap_lang/lib/spawn.v
 theories/heap_lang/lib/par.v
 theories/heap_lang/lib/assert.v
@@ -86,9 +89,7 @@ theories/heap_lang/lib/spin_lock.v
 theories/heap_lang/lib/ticket_lock.v
 theories/heap_lang/lib/counter.v
 theories/heap_lang/lib/atomic_heap.v
-theories/heap_lang/proofmode.v
-theories/heap_lang/adequacy.v
-theories/heap_lang/total_adequacy.v
+theories/heap_lang/lib/increment.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v

theories/bi/lib/atomic.v

@@ -10,8 +10,8 @@ Definition atomic_shift {PROP: sbi} `{!FUpd PROP} {A B : Type}
   (P : PROP) (* pre-condition *)
   (Q : A → B → PROP) (* post-condition *)
   : PROP :=
-    (□ (∀ E, ⌜Eo ⊆ E⌝ -∗ ▷ P ={E, E∖Em}=∗ ∃ x, α x ∗
-          ((α x ={E∖Em, E}=∗ ▷ P) ∧ (∀ y, β x y ={E∖Em, E}=∗ Q x y)))
+    (□ (∀ E, ⌜Eo ⊆ E⌝ -∗ P ={E, E∖Em}=∗ ∃ x, α x ∗
+          ((α x ={E∖Em, E}=∗ P) ∧ (∀ y, β x y ={E∖Em, E}=∗ Q x y)))
     )%I.
 
 Definition atomic_update {PROP: sbi} `{!FUpd PROP} {A B : Type}
@@ -21,7 +21,7 @@ Definition atomic_update {PROP: sbi} `{!FUpd PROP} {A B : Type}
   (Q : A → B → PROP) (* post-condition *)
   : PROP :=
     tc_opaque (
-      ∃ (F P : PROP), F ∗ ▷ P ∗ atomic_shift α β Eo Em P (λ x y, F -∗ Q x y)
+      ∃ (F P : PROP), F ∗ ▷ P ∗ atomic_shift α β Eo Em (▷ P) (λ x y, F -∗ Q x y)
     )%I.
 
 Section lemmas.

theories/heap_lang/lib/atomic_heap.v

@@ -6,7 +6,7 @@ From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
 (** A general logically atomic interface for a heap. *)
-Structure atomic_heap Σ `{!heapG Σ} := AtomicHeap {
+Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   (* -- operations -- *)
   alloc : val;
   load : val;
@@ -26,19 +26,22 @@ Structure atomic_heap Σ `{!heapG Σ} := AtomicHeap {
               (λ '(v, q) (_:()), mapsto l q v)
               ⊤ ∅
               (λ '(v, q) _, v);
-  store_spec (l : loc) (w : val) :
-    atomic_wp (store (#l, w))%E
+  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) (w1 w2 : val) :
-    atomic_wp (cas (#l, w1, w2))%E
+  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 _ {_}.
 
 (** Proof that the primitive physical operations of heap_lang satisfy said interface. *)
 Definition primitive_alloc : val :=
@@ -71,26 +74,28 @@ Section proof.
     wp_load. iMod ("Hclose" $! () with "H↦"). done.
   Qed.
 
-  Lemma primitive_store_spec (l : loc) (w : val) :
-    atomic_wp (primitive_store (#l, w))%E
+  Lemma primitive_store_spec (l : loc) (e : expr) (w : val) :
+    IntoVal e w →
+    atomic_wp (primitive_store (#l, e))%E
               (λ v, l ↦ v)%I
               (λ v (_:()), l ↦ w)%I
               ⊤ ∅
               (λ _ _, #()%V).
   Proof.
-    iIntros (Φ) "Aupd". wp_let. wp_proj. wp_proj.
+    iIntros (<-%of_to_val Φ) "Aupd". wp_let. wp_proj. wp_proj.
     iMod (aupd_acc with "Aupd") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
     wp_store. iMod ("Hclose" $! () with "H↦"). done.
   Qed.
 
-  Lemma primitive_cas_spec (l : loc) (w1 w2 : val) :
-    atomic_wp (primitive_cas (#l, w1, w2))%E
+  Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
+    IntoVal e1 w1 → IntoVal e2 w2 →
+    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 (Φ) "Aupd". wp_let. repeat wp_proj.
+    iIntros (<-%of_to_val <-%of_to_val Φ) "Aupd". wp_let. repeat wp_proj.
     iMod (aupd_acc with "Aupd") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
     destruct (decide (v = w1)) as [Hv|Hv]; [wp_cas_suc|wp_cas_fail];
     iMod ("Hclose" $! () with "H↦"); done.

theories/heap_lang/lib/increment.v

+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.
+Set Default Proof Using "Type".
+
+(** Show taht implementing fetch-and-add on top of CAS preserves logical
+atomicity. *)
+
+(* TODO: Move this to iris-examples once gen_proofmode is merged. *)
+Section increment.
+  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
+
+  Definition incr: val :=
+    rec: "incr" "l" :=
+       let: "oldv" := aheap.(load) "l" in
+       if: aheap.(cas) ("l", "oldv", ("oldv" + #1))
+         then "oldv" (* return old value if success *)
+         else "incr" "l".
+
+  Lemma incr_spec (l: loc) :
+        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.
+    wp_apply load_spec.
+    (* Prove the atomic shift for load *)
+    iDestruct "AUpd" as (F P) "(HF & HP & #AShft)".
+    iExists F, P. iFrame. iIntros "!# * % HP".
+    iMod ("AShft" with "[%] HP") as (x) "[H↦ Hclose]"; first done.
+    iModIntro. iExists (#x, 1%Qp). iFrame. iSplit.
+    { iDestruct "Hclose" as "[Hclose _]". iApply "Hclose". }
+    iIntros (_) "H↦". iDestruct "Hclose" as "[Hclose _]".
+    iMod ("Hclose" with "H↦") as "HP". iIntros "!> HF".
+    clear dependent E.
+    (* Now go on *)
+    wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
+    wp_apply cas_spec.
+    (* Prove the atomic shift for CAS *)
+    iExists F, P. iFrame. iIntros "!# * % HP".
+    iMod ("AShft" with "[%] HP") as (x') "[H↦ Hclose]"; first done.
+    iModIntro. iExists #x'. iFrame. iSplit.
+    { iDestruct "Hclose" as "[Hclose _]". iApply "Hclose". }
+    iIntros (_). destruct (decide (#x' = #x)) as [[= Hx]|Hx].
+    - iIntros "H↦". iDestruct "Hclose" as "[_ Hclose]". subst.
+      iMod ("Hclose" $! () with "H↦") as "HΦ". iIntros "!> HF".
+      wp_if. by iApply "HΦ".
+    - iDestruct "Hclose" as "[Hclose _]". iIntros "H↦".
+      iMod ("Hclose" with "H↦") as "HP". iIntros "!> HF".
+      wp_if. iApply "IH". iExists F, P. iFrame. done.
+  Qed.
+
+End increment.
+