add 'atomic triple' for compare-and-set, and use it in one example

_CoqProject

@@ -115,6 +115,7 @@ theories/heap_lang/lib/lazy_coin.v
 theories/heap_lang/lib/counter.v
 theories/heap_lang/lib/atomic_heap.v
 theories/heap_lang/lib/increment.v
+theories/heap_lang/lib/compare_and_set.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v

theories/heap_lang/lib/compare_and_set.v

+From iris.heap_lang Require Export lifting notation.
+From iris.program_logic Require Export atomic.
+From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type".
+
+(* Defines compare-and-set (CASet) on top of compare-and-swap (CAS). *)
+
+Definition compare_and_set : val :=
+  λ: "l" "v1" "v2", CAS "l" "v1" "v2" = "v1".
+
+Section proof.
+  Context `{!heapG Σ}.
+
+  (* This is basically a logically atomic spec, but stronger and hence easier to apply. *)
+  Lemma caset_spec (l : loc) (v1 v2 : val) Φ E :
+    val_is_unboxed v1 →
+    (|={⊤,E}=> ∃ v, l ↦ v ∗ let b := bool_decide (val_for_compare v = val_for_compare v1) in
+        (l ↦ (if b then v2 else v) ={E,⊤}=∗ Φ #b) ) -∗
+    WP compare_and_set #l v1 v2 @ ⊤ {{ Φ }}.
+  Proof.
+    iIntros (?) "AU". wp_lam. wp_pures. wp_bind (CAS _ _ _).
+    iMod "AU" as (v) "[H↦ Hclose]". case_bool_decide.
+    - wp_cas_suc. iMod ("Hclose" with "H↦"). iModIntro. wp_op.
+      rewrite bool_decide_true //.
+    - wp_cas_fail. iMod ("Hclose" with "H↦"). iModIntro. wp_op.
+      rewrite bool_decide_false //.
+  Qed.
+End proof.

theories/heap_lang/lib/counter.v

@@ -3,13 +3,13 @@ From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac_auth auth.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Import proofmode notation lib.compare_and_set.
 Set Default Proof Using "Type".
 
 Definition newcounter : val := λ: <>, ref #0.
 Definition incr : val := rec: "incr" "l" :=
     let: "n" := !"l" in
-    if: CAS "l" "n" (#1 + "n") = "n" then #() else "incr" "l".
+    if: compare_and_set "l" "n" (#1 + "n") then #() else "incr" "l".
 Definition read : val := λ: "l", !"l".
 
 (** Monotone counter *)
@@ -50,25 +50,25 @@ Section mono_proof.
     iDestruct "Hl" as (γ) "[#? Hγf]".
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
     wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    wp_pures.
-    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
+    wp_pures. wp_apply caset_spec; first done.
+    iInv N as (c') ">[Hγ Hl]" "Hclose".
     destruct (decide (c' = c)) as [->|].
     - iDestruct (own_valid_2 with "Hγ Hγf")
         as %[?%mnat_included _]%auth_both_valid.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
-      wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
-      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      wp_op. rewrite bool_decide_true //. wp_if.
+      iExists _; iFrame "Hl". iIntros "!> Hl".
+      rewrite bool_decide_true //. iMod ("Hclose" with "[Hl Hγ]") as "_".
+      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. iFrame. }
+      iModIntro. wp_if.
       iApply "HΦ"; iExists γ; repeat iSplit; eauto.
       iApply (own_mono with "Hγf").
       (* FIXME: FIXME(Coq #6294): needs new unification *)
       apply: auth_frag_mono. by apply mnat_included, le_n_S.
-    - assert (#c ≠ #c') by by intros [= ?%Nat2Z.inj].
-      wp_cas_fail. iModIntro.
-      iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
-      wp_op. rewrite bool_decide_false //. wp_if.
-      iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
+    - iExists _; iFrame "Hl". iIntros "!> Hl".
+      rewrite bool_decide_false; last by intros [= ?%Nat2Z.inj].
+      iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
+      iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
       rewrite {3}/mcounter; eauto 10.
   Qed.
 
@@ -132,18 +132,19 @@ Section contrib_spec.
     iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
     wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    wp_pures.
-    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
+    wp_pures. wp_apply caset_spec; first done.
+    iInv N as (c') ">[Hγ Hl]" "Hclose".
     destruct (decide (c' = c)) as [->|].
     - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
-      wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
+      iExists _; iFrame "Hl". iIntros "!> Hl".
+      rewrite bool_decide_true //. iMod ("Hclose" with "[Hl Hγ]") as "_".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      wp_op. rewrite bool_decide_true //. wp_if. by iApply "HΦ".
-    - assert (#c ≠ #c') by by intros [= ?%Nat2Z.inj]. wp_cas_fail.
-      iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
-      wp_op. rewrite bool_decide_false //. wp_if.
-      by iApply ("IH" with "[Hγf] [HΦ]"); auto.
+      iModIntro. wp_if. by iApply "HΦ".
+    - iExists _; iFrame "Hl". iIntros "!> Hl".
+      rewrite bool_decide_false; last by intros [= ?%Nat2Z.inj].
+      iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
+      iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
   Qed.
 
   Lemma read_contrib_spec γ l q n :