diff --git a/CHANGELOG.md b/CHANGELOG.md
index 27a81b79d4e4babb716e01ac1ad9f342f15745ac..3d7e8bc1bda7cd3cd533f1ccb04dfb8ae7b2c794 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -54,6 +54,12 @@ Changes in heap_lang:
   "normalized" to the same.  This makes all closures indistinguishable from each
   other while remaining unqueal to anything else.  We also use the same
   "normalization" to make sure all prophecy variables seem equal to `()`.
+* CAS (compare-and-set) got replaced by CmpXchg (compare-exchange).  The
+  difference is that CmpXchg returns a pair consisting of the old value and a
+  boolean indicating whether the comparison was successful and hence the
+  exchange happened.  CAS can be obtained by simply projecting to the second
+  component, but also providing the old value more closely models the primitive
+  typically provided in systems languages (C, C++, Rust).
 
 Changes in Coq:
 
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 0b4905002c9450b94bcdc45a01dfaf04fb01ac8a..eaaa3c9630f329329bd4abef67ef0e964d8701fc 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -40,7 +40,7 @@
   ============================
   _ : ▷ l ↦ #0
   --------------------------------------∗
-  WP CAS #l #0 #1 {{ _, l ↦ #1 }}
+  WP CmpXchg #l #0 #1 {{ _, l ↦ #1 }}
   
 1 subgoal
   
@@ -144,8 +144,9 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
     let: "val2" := fun2 "val1" in
     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
-"not_cas"
+"not_cmpxchg"
      : string
 The command has indeed failed with message:
-Ltac call to "wp_cas_suc" failed.
-Tactic failure: wp_cas_suc: cannot find 'CAS' in (#() #()).
+Ltac call to "wp_cmpxchg_suc" failed.
+Tactic failure: wp_cmpxchg_suc: cannot find 'CmpXchg' in 
+(#() #()).
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index ebde315ef532338106d2e92fd940d5ec72464eaf..df044f7f6d4ec56174dd9ca1ce28d59c756362b0 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -79,14 +79,14 @@ Section tests.
   Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, ⌜ w = #true ⌝ }})%I.
   Proof. wp_lam. wp_op. by case_bool_decide. Qed.
 
-  Definition heap_e7 : val := λ: "v", CAS "v" #0 #1.
+  Definition heap_e7 : val := λ: "v", CmpXchg "v" #0 #1.
 
   Lemma heap_e7_spec_total l : l ↦ #0 -∗ WP heap_e7 #l [{_,  l ↦ #1 }].
-  Proof. iIntros. wp_lam. wp_cas_suc. auto. Qed.
+  Proof. iIntros. wp_lam. wp_cmpxchg_suc. auto. Qed.
 
   Check "heap_e7_spec".
   Lemma heap_e7_spec l : ▷^2 l ↦ #0 -∗ WP heap_e7 #l {{_,  l ↦ #1 }}.
-  Proof. iIntros. wp_lam. Show. wp_cas_suc. Show. auto. Qed.
+  Proof. iIntros. wp_lam. Show. wp_cmpxchg_suc. Show. auto. Qed.
 
   Definition FindPred : val :=
     rec: "pred" "x" "y" :=
@@ -124,11 +124,11 @@ Section tests.
     P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
   Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
 
-  Lemma wp_cas l v :
+  Lemma wp_cmpxchg l v :
     val_is_unboxed v →
-    l ↦ v -∗ WP CAS #l v v {{ _, True }}.
+    l ↦ v -∗ WP CmpXchg #l v v {{ _, True }}.
   Proof.
-    iIntros (?) "?". wp_cas as ? | ?. done. done.
+    iIntros (?) "?". wp_cmpxchg as ? | ?. done. done.
   Qed.
 
   Lemma wp_alloc_split :
@@ -210,11 +210,11 @@ End printing_tests.
 Section error_tests.
   Context `{!heapG Σ}.
 
-  Check "not_cas".
-  Lemma not_cas :
+  Check "not_cmpxchg".
+  Lemma not_cmpxchg :
     (WP #() #() {{ _, True }})%I.
   Proof.
-    Fail wp_cas_suc.
+    Fail wp_cmpxchg_suc.
   Abort.
 End error_tests.
 
diff --git a/tests/heap_lang_proph.v b/tests/heap_lang_proph.v
index 4c27474998c30abf7ba576308b9528881e53012c..109958a5c95ecef365280e11671ff4835e5bc21f 100644
--- a/tests/heap_lang_proph.v
+++ b/tests/heap_lang_proph.v
@@ -8,46 +8,22 @@ Section tests.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val → iProp Σ.
 
-  Definition CAS_resolve e1 e2 e3 p v :=
-    Resolve (CAS e1 e2 e3) p v.
-
-  Lemma wp_cas_suc_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v1 v2 v : val) :
-    vals_cas_compare_safe v1 v1 →
-    {{{ proph p vs ∗ ▷ l ↦ v1 }}}
-      CAS_resolve #l v1 v2 #p v @ s; E
-    {{{ RET #true ; ∃ vs', ⌜vs = (#true, v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v2 }}}.
-  Proof.
-    iIntros (Hcmp Φ) "[Hp Hl] HΦ".
-    wp_apply (wp_resolve with "Hp"); first done.
-    assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
-    wp_cas_suc. iIntros (vs' ->) "Hp".
-    iApply "HΦ". eauto with iFrame.
-  Qed.
-
-  Lemma wp_cas_fail_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v' v1 v2 v : val) :
-    val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
-    {{{ proph p vs ∗ ▷ l ↦ v' }}}
-      CAS_resolve #l v1 v2 #p v @ s; E
-    {{{ RET #false ; ∃ vs', ⌜vs = (#false, v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v' }}}.
-  Proof.
-    iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
-    wp_apply (wp_resolve with "Hp"); first done.
-    wp_cas_fail. iIntros (vs' ->) "Hp".
-    iApply "HΦ". eauto with iFrame.
-  Qed.
-
   Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
     l ↦ #n -∗
     proph p vs -∗
-    WP Resolve (CAS #l #n (#n + #1)) #p v @ E {{ v, ⌜v = #true⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}%I.
+    WP Resolve (CmpXchg #l #n (#n + #1)) #p v @ E
+      {{ v, ⌜v = (#n, #true)%V⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}.
   Proof.
     iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
-    wp_cas_suc. iIntros (ws ->) "Hp". eauto with iFrame.
+    wp_cmpxchg_suc. iIntros (ws ->) "Hp". eauto with iFrame.
+  Restart.
+    iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve_cmpxchg_suc with "[$Hp $Hl]"); first by left.
+    iIntros "Hpost". iDestruct "Hpost" as (ws ->) "Hp". eauto with iFrame.
   Qed.
 
   Lemma test_resolve2 E (l : loc) (n m : Z) (p : proph_id) (vs : list (val * val)) :
     proph p vs -∗
-    WP Resolve (#n + #m - (#n + #m)) #p #() @ E {{ v, ⌜v = #0⌝ ∗ ∃vs, proph p vs }}%I.
+    WP Resolve (#n + #m - (#n + #m)) #p #() @ E {{ v, ⌜v = #0⌝ ∗ ∃vs, proph p vs }}.
   Proof.
     iIntros "Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
     wp_pures. iIntros (ws ->) "Hp". rewrite Z.sub_diag. eauto with iFrame.
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 3db32f442b61ca098c2ee674eda27e4449bd1bd5..79ec0d82a344c5adb38d4b01c18b18cea2973f3e 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -222,19 +222,19 @@ Section counter_proof.
     iDestruct 1 as (c) "[Hl Hγ]".
     wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     wp_let. wp_op.
-    wp_bind (CAS _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto.
+    wp_bind (CmpXchg _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto.
     iDestruct 1 as (c') ">[Hl Hγ]".
     destruct (decide (c' = c)) as [->|].
     - iCombine "Hγ" "Hγf" as "Hγ".
       iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
       iMod (own_update with "Hγ") as "Hγ"; first apply M_update.
       rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
-      wp_cas_suc. iSplitL "Hl Hγ".
+      wp_cmpxchg_suc. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      wp_if. rewrite {3}/C; eauto 10.
-    - wp_cas_fail; first (intros [=]; abstract omega).
+      wp_pures. rewrite {3}/C; eauto 10.
+    - wp_cmpxchg_fail; first (intros [=]; abstract omega).
       iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
-      wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
+      wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
   Qed.
 
   Check "read_spec".
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 8230e955044672960fb51fa289432b2e1f856c65..01159f1a77a05459cdbb1acd0a4d7f9999bf6755 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -49,13 +49,13 @@ Proof.
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
   { iNext. iLeft. by iSplitL "Hl". }
   wp_pures. iModIntro. iApply "Hf"; iSplit.
-  - iIntros (n) "!#". wp_lam. wp_pures.
+  - iIntros (n) "!#". wp_lam. wp_pures. wp_bind (CmpXchg _ _ _).
     iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
     + iMod (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Shot n). }
-      wp_cas_suc. iSplitL; last eauto.
-      iModIntro. iNext; iRight; iExists n; by iFrame.
-    + wp_cas_fail. iSplitL; last eauto.
+      wp_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
+      iNext; iRight; iExists n; by iFrame.
+    + wp_cmpxchg_fail. iModIntro. iSplitL; last (wp_pures; by eauto).
       rewrite /one_shot_inv; eauto 10.
   - iIntros "!# /=". wp_lam. wp_bind (! _)%E.
     iInv N as ">Hγ".
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index bef6a6bb302d6c0183763ebc70504663315ae221..84ac31eac7fd4528ead83ab637f24118e4fa156f 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -28,11 +28,11 @@ the [Resolve] is stuck), and this value is also attached to the resolution.
 A prophecy variable is thus resolved to a pair containing (1) the result
 value of the wrapped expression (called [e] above), and (2) the value that
 was attached by the [Resolve] (called [v] above). This allows, for example,
-to distinguish a resolution originating from a successful [CAS] from one
-originating from a failing [CAS]. For example:
- - [Resolve (CAS #l #n #(n+1)) #p v] will behave as [CAS #l #n #(n+1)],
-   which means step to a boolean [b] while updating the heap, but in the
-   meantime the prophecy variable [p] will be resolved to [(#b, v)].
+to distinguish a resolution originating from a successful [CmpXchg] from one
+originating from a failing [CmpXchg]. For example:
+ - [Resolve (CmpXchg #l #n #(n+1)) #p v] will behave as [CmpXchg #l #n #(n+1)],
+   which means step to a value-boole pair [(n', b)] while updating the heap, but
+   in the meantime the prophecy variable [p] will be resolved to [(n', b), v)].
  - [Resolve (! #l) #p v] will behave as [! #l], that is return the value
    [w] pointed to by [l] on the heap (assuming it was allocated properly),
    but it will additionally resolve [p] to the pair [(w,v)].
@@ -41,10 +41,10 @@ Note that the sub-expressions of [Resolve e p v] (i.e., [e], [p] and [v])
 are reduced as usual, from right to left. However, the evaluation of [e]
 is restricted so that the head-step to which the resolution is attached
 cannot be taken by the context. For example:
- - [Resolve (CAS #l #n (#n + #1)) #p v] will first be reduced (with by a
-   context-step) to [Resolve (CAS #l #n #(n+1) #p v], and then behave as
+ - [Resolve (CmpXchg #l #n (#n + #1)) #p v] will first be reduced (with by a
+   context-step) to [Resolve (CmpXchg #l #n #(n+1) #p v], and then behave as
    described above.
- - However, [Resolve ((λ: "n", CAS #l "n" ("n" + #1)) #n) #p v] is stuck.
+ - However, [Resolve ((λ: "n", CmpXchg #l "n" ("n" + #1)) #n) #p v] is stuck.
    Indeed, it can only be evaluated using a head-step (it is a β-redex),
    but the process does not yield a value.
 
@@ -97,8 +97,8 @@ Inductive expr :=
   | AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
-  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
-  | FAA (e1 : expr) (e2 : expr)
+  | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-exchange *)
+  | FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *)
   (* Prophecy *)
   | NewProph
   | Resolve (e0 : expr) (e1 : expr) (e2 : expr) (* wrapped expr, proph, val *)
@@ -115,7 +115,7 @@ Bind Scope val_scope with val.
 (** An observation associates a prophecy variable (identifier) to a pair of
 values. The first value is the one that was returned by the (atomic) operation
 during which the prophecy resolution happened (typically, a boolean when the
-wrapped operation is a CAS). The second value is the one that the prophecy
+wrapped operation is a CmpXchg). The second value is the one that the prophecy
 variable was actually resolved to. *)
 Definition observation : Set := proph_id * (val * val).
 
@@ -159,13 +159,13 @@ Definition val_is_unboxed (v : val) : Prop :=
   | _ => False
   end.
 
-(** CAS just compares the word-sized representation of two values, it cannot
+(** CmpXchg just compares the word-sized representation of two values, it cannot
 look into boxed data.  This works out fine if at least one of the to-be-compared
 values is unboxed (exploiting the fact that an unboxed and a boxed value can
 never be equal because these are disjoint sets). *)
-Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
+Definition vals_cmpxchg_compare_safe (vl v1 : val) : Prop :=
   val_is_unboxed vl ∨ val_is_unboxed v1.
-Arguments vals_cas_compare_safe !_ !_ /.
+Arguments vals_cmpxchg_compare_safe !_ !_ /.
 
 (** We don't compare the logical program values, but we first normalize them
 to make sure that prophecies are treated like unit.
@@ -235,7 +235,7 @@ Proof.
      | Load e, Load e' => cast_if (decide (e = e'))
      | Store e1 e2, Store e1' e2' =>
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
-     | CAS e0 e1 e2, CAS e0' e1' e2' =>
+     | CmpXchg e0 e1 e2, CmpXchg e0' e1' e2' =>
         cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
      | FAA e1 e2, FAA e1' e2' =>
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
@@ -311,7 +311,7 @@ Proof.
      | AllocN e1 e2 => GenNode 13 [go e1; go e2]
      | Load e => GenNode 14 [go e]
      | Store e1 e2 => GenNode 15 [go e1; go e2]
-     | CAS e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
+     | CmpXchg e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
      | FAA e1 e2 => GenNode 17 [go e1; go e2]
      | NewProph => GenNode 18 []
      | Resolve e0 e1 e2 => GenNode 19 [go e0; go e1; go e2]
@@ -346,7 +346,7 @@ Proof.
      | GenNode 13 [e1; e2] => AllocN (go e1) (go e2)
      | GenNode 14 [e] => Load (go e)
      | GenNode 15 [e1; e2] => Store (go e1) (go e2)
-     | GenNode 16 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
+     | GenNode 16 [e0; e1; e2] => CmpXchg (go e0) (go e1) (go e2)
      | GenNode 17 [e1; e2] => FAA (go e1) (go e2)
      | GenNode 18 [] => NewProph
      | GenNode 19 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
@@ -401,9 +401,9 @@ Inductive ectx_item :=
   | LoadCtx
   | StoreLCtx (v2 : val)
   | StoreRCtx (e1 : expr)
-  | CasLCtx (v1 : val) (v2 : val)
-  | CasMCtx (e0 : expr) (v2 : val)
-  | CasRCtx (e0 : expr) (e1 : expr)
+  | CmpXchgLCtx (v1 : val) (v2 : val)
+  | CmpXchgMCtx (e0 : expr) (v2 : val)
+  | CmpXchgRCtx (e0 : expr) (e1 : expr)
   | FaaLCtx (v2 : val)
   | FaaRCtx (e1 : expr)
   | ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val)
@@ -414,8 +414,8 @@ Inductive ectx_item :=
 the local context of [e] is non-empty. As a consequence, the first argument of
 [Resolve] is not completely evaluated (down to a value) by contextual closure:
 no head steps (i.e., surface reductions) are taken. This means that contextual
-closure will reduce [Resolve (CAS #l #n (#n + #1)) #p #v] into [Resolve (CAS
-#l #n #(n+1)) #p #v], but it cannot context-step any further. *)
+closure will reduce [Resolve (CmpXchg #l #n (#n + #1)) #p #v] into [Resolve
+(CmpXchg #l #n #(n+1)) #p #v], but it cannot context-step any further. *)
 
 Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
   match Ki with
@@ -437,9 +437,9 @@ Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
   | LoadCtx => Load e
   | StoreLCtx v2 => Store e (Val v2)
   | StoreRCtx e1 => Store e1 e
-  | CasLCtx v1 v2 => CAS e (Val v1) (Val v2)
-  | CasMCtx e0 v2 => CAS e0 e (Val v2)
-  | CasRCtx e0 e1 => CAS e0 e1 e
+  | CmpXchgLCtx v1 v2 => CmpXchg e (Val v1) (Val v2)
+  | CmpXchgMCtx e0 v2 => CmpXchg e0 e (Val v2)
+  | CmpXchgRCtx e0 e1 => CmpXchg e0 e1 e
   | FaaLCtx v2 => FAA e (Val v2)
   | FaaRCtx e1 => FAA e1 e
   | ResolveLCtx K v1 v2 => Resolve (fill_item K e) (Val v1) (Val v2)
@@ -468,7 +468,7 @@ Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
   | AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
   | Load e => Load (subst x v e)
   | Store e1 e2 => Store (subst x v e1) (subst x v e2)
-  | CAS e0 e1 e2 => CAS (subst x v e0) (subst x v e1) (subst x v e2)
+  | CmpXchg e0 e1 e2 => CmpXchg (subst x v e0) (subst x v e1) (subst x v e2)
   | FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
   | NewProph => NewProph
   | Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2)
@@ -518,6 +518,7 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
 
 Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
   if decide (op = EqOp) then
+    (* Crucially, this compares the same way as [CmpXchg]! *)
     Some $ LitV $ LitBool $ bool_decide (val_for_compare v1 = val_for_compare v2)
   else
     match v1, v2 with
@@ -633,19 +634,14 @@ Inductive head_step : expr → state → list observation → expr → state →
                []
                (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
                []
-  | CasFailS l v1 v2 vl σ :
-     vals_cas_compare_safe vl v1 →
+  | CmpXchgS l v1 v2 vl σ b :
+     vals_cmpxchg_compare_safe vl v1 →
      σ.(heap) !! l = Some vl →
-     val_for_compare vl ≠ val_for_compare v1 →
-     head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ []
-               (Val $ LitV $ LitBool false) σ []
-  | CasSucS l v1 v2 vl σ :
-     vals_cas_compare_safe vl v1 →
-     σ.(heap) !! l = Some vl →
-     val_for_compare vl = val_for_compare v1 →
-     head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
+     (* Crucially, this compares the same way as [EqOp]! *)
+     b = bool_decide (val_for_compare vl = val_for_compare v1) →
+     head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
                []
-               (Val $ LitV $ LitBool true) (state_upd_heap <[l:=v2]> σ)
+               (Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=v2]> σ else σ)
                []
   | FaaS l i1 i2 σ :
      σ.(heap) !! l = Some (LitV (LitInt i1)) →
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index 57178712a330d48bc7d324f57f6241f3f6ca997a..fc059f5c95069f73204b88aa5d3dca19e52701d2 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -11,7 +11,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   alloc : val;
   load : val;
   store : val;
-  cas : val;
+  cmpxchg : val;
   (* -- predicates -- *)
   mapsto (l : loc) (q: Qp) (v : val) : iProp Σ;
   (* -- mapsto properties -- *)
@@ -31,12 +31,14 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   (* This spec is slightly weaker than it could be: It is sufficient for [w1]
   *or* [v] to be unboxed.  However, by writing it this way the [val_is_unboxed]
   is outside the atomic triple, which makes it much easier to use -- and the
-  spec is still good enough for all our applications. *)
-  cas_spec (l : loc) (w1 w2 : val) :
+  spec is still good enough for all our applications.
+  The postcondition deliberately does not use [bool_decide] so that users can
+  [destruct (decide (a = b))] and it will simplify in both places. *)
+  cmpxchg_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    <<< ∀ v, mapsto l 1 v >>> cas #l w1 w2 @ ⊤
+    <<< ∀ v, mapsto l 1 v >>> cmpxchg #l w1 w2 @ ⊤
     <<< if decide (val_for_compare v = val_for_compare w1) then mapsto l 1 w2 else mapsto l 1 v,
-        RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>;
+        RET (v, #if decide (val_for_compare v = val_for_compare w1) then true else false) >>>;
 }.
 Arguments atomic_heap _ {_}.
 
@@ -54,10 +56,28 @@ Notation "'ref' e" := (alloc e) : expr_scope.
 Notation "! e" := (load e) : expr_scope.
 Notation "e1 <- e2" := (store e1 e2) : expr_scope.
 
-Notation CAS e1 e2 e3 := (cas e1 e2 e3).
+Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
 
 End notation.
 
+Section derived.
+  Context `{!heapG Σ, !atomic_heap Σ}.
+
+  Import notation.
+
+  Lemma cas_spec (l : loc) (w1 w2 : val) :
+    val_is_unboxed w1 →
+    <<< ∀ v, mapsto l 1 v >>> CAS #l w1 w2 @ ⊤
+    <<< if decide (val_for_compare v = val_for_compare w1) then mapsto l 1 w2 else mapsto l 1 v,
+        RET #if decide (val_for_compare v = val_for_compare w1) then true else false >>>.
+  Proof.
+    iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done.
+    iApply (aacc_aupd_commit with "AU"); first done.
+    iIntros (v) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
+    iIntros "$ !> HΦ !>". wp_pures. done.
+  Qed.
+End derived.
+
 (** Proof that the primitive physical operations of heap_lang satisfy said interface. *)
 Definition primitive_alloc : val :=
   λ: "v", ref "v".
@@ -65,8 +85,8 @@ Definition primitive_load : val :=
   λ: "l", !"l".
 Definition primitive_store : val :=
   λ: "l" "x", "l" <- "x".
-Definition primitive_cas : val :=
-  λ: "l" "e1" "e2", CAS "l" "e1" "e2".
+Definition primitive_cmpxchg : val :=
+  λ: "l" "e1" "e2", CmpXchg "l" "e1" "e2".
 
 Section proof.
   Context `{!heapG Σ}.
@@ -95,17 +115,17 @@ Section proof.
     wp_store. iMod ("Hclose" with "H↦") as "HΦ". done.
   Qed.
 
-  Lemma primitive_cas_spec (l : loc) (w1 w2 : val) :
+  Lemma primitive_cmpxchg_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
     <<< ∀ (v : val), l ↦ v >>>
-      primitive_cas #l w1 w2 @ ⊤
+      primitive_cmpxchg #l w1 w2 @ ⊤
     <<< if decide (val_for_compare v = val_for_compare w1) then l ↦ w2 else l ↦ v,
-        RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>.
+        RET (v, #if decide (val_for_compare v = val_for_compare w1) then true else false) >>>.
   Proof.
-    iIntros (? Φ) "AU". wp_lam. wp_let. wp_let.
+    iIntros (? Φ) "AU". wp_lam. wp_pures.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
     destruct (decide (val_for_compare v = val_for_compare w1)) as [Heq|Hne];
-      [wp_cas_suc|wp_cas_fail];
+      [wp_cmpxchg_suc|wp_cmpxchg_fail];
     iMod ("Hclose" with "H↦") as "HΦ"; done.
   Qed.
 End proof.
@@ -116,5 +136,5 @@ Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
   {| alloc_spec := primitive_alloc_spec;
      load_spec := primitive_load_spec;
      store_spec := primitive_store_spec;
-     cas_spec := primitive_cas_spec;
+     cmpxchg_spec := primitive_cmpxchg_spec;
      mapsto_agree := gen_heap.mapsto_agree  |}.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 221a89f84769247d351f2b88be3096e86bdc80a7..4b7058988290aa68957ca306c2dfbbf50ef5030a 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -50,22 +50,22 @@ 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_bind (CmpXchg _ _ _).
+    iInv N as (c') ">[Hγ Hl]".
     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γ".
+      wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
+      wp_pures. 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.
-    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
+    - wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
       iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
-      wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
+      wp_pures. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
       rewrite {3}/mcounter; eauto 10.
   Qed.
 
@@ -129,17 +129,17 @@ 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_bind (CmpXchg _ _ _).
+    iInv N as (c') ">[Hγ Hl]".
     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γ".
+      wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      wp_if. by iApply "HΦ".
-    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
+      wp_pures. by iApply "HΦ".
+    - wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]).
       iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
-      wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
+      wp_pures. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
   Qed.
 
   Lemma read_contrib_spec γ l q n :
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index ee949dba512f973a6877ca93783f13fb1fd373ae..00065aa8db13d86a5800827e900acf787c7604ef 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -26,12 +26,12 @@ Section increment_physical.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
     wp_load. iMod ("Hclose" with "Hl") as "AU". iModIntro.
-    wp_pures. wp_bind (CAS _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
+    wp_pures. wp_bind (CmpXchg _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
     destruct (decide (#v = #w)) as [[= ->]|Hx].
-    - wp_cas_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
-      iModIntro. wp_if. done.
-    - wp_cas_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
-      iModIntro. wp_if. iApply "IH". done.
+    - wp_cmpxchg_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
+      iModIntro. wp_pures. done.
+    - wp_cmpxchg_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
+      iModIntro. wp_pures. iApply "IH". done.
   Qed.
 End increment_physical.
 
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 695cd759a9feb025dffa2eb185dbafc5db2bf1d2..3370bdcc298b5bb75baf9bcadd318512c61d9ca1 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -61,12 +61,12 @@ Section proof.
     {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
   Proof.
     iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
-    wp_rec. iInv N as ([]) "[Hl HR]".
-    - wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
-      iApply ("HΦ" $! false). done.
-    - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
+    wp_rec. wp_bind (CmpXchg _ _ _). iInv N as ([]) "[Hl HR]".
+    - wp_cmpxchg_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
+      wp_pures. iApply ("HΦ" $! false). done.
+    - wp_cmpxchg_suc. iDestruct "HR" as "[Hγ HR]".
       iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
-      rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
+      rewrite /locked. wp_pures. by iApply ("HΦ" $! true with "[$Hγ $HR]").
   Qed.
 
   Lemma acquire_spec γ lk R :
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 0fb6f0aa8047e5720e640c202f34b07a04393795..5600f18d9fd5495eb91bbe97dd9723755b8dfdcf 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -111,7 +111,7 @@ Section proof.
     iInv N as (o n) "[Hlo [Hln Ha]]".
     wp_load. iModIntro. iSplitL "Hlo Hln Ha".
     { iNext. iExists o, n. by iFrame. }
-    wp_pures. wp_bind (CAS _ _ _).
+    wp_pures. wp_bind (CmpXchg _ _ _).
     iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
     destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
     - iMod (own_update with "Hauth") as "[Hauth Hofull]".
@@ -119,17 +119,17 @@ Section proof.
         eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
         apply (set_seq_S_end_disjoint 0). }
       rewrite -(set_seq_S_end_union_L 0).
-      wp_cas_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
+      wp_cmpxchg_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
       { iNext. iExists o', (S n).
         rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
-      wp_if.
+      wp_pures.
       iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
       + iFrame. rewrite /is_lock; eauto 10.
       + by iNext.
-    - wp_cas_fail. iModIntro.
+    - wp_cmpxchg_fail. iModIntro.
       iSplitL "Hlo' Hln' Hauth Haown".
       { iNext. iExists o', n'. by iFrame. }
-      wp_if. by iApply "IH"; auto.
+      wp_pures. by iApply "IH"; auto.
   Qed.
 
   Lemma release_spec γ lk R :
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 4414aa1de2a9abf1d4dbdcb5207b95c72dfd46b8..7df88724965f5296c1fbd0a7ab4140bac1d5c367 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -56,8 +56,7 @@ Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core
 
 (* [simpl apply] is too stupid, so we need extern hints here. *)
 Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
-Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS : core.
-Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS : core.
+Local Hint Extern 0 (head_step (CmpXchg _ _ _) _ _ _ _ _) => eapply CmpXchgS : core.
 Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core.
 Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
 Local Hint Resolve to_of_val : core.
@@ -78,7 +77,7 @@ Instance load_atomic s v : Atomic s (Load (Val v)).
 Proof. solve_atomic. Qed.
 Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
 Proof. solve_atomic. Qed.
-Instance cas_atomic s v0 v1 v2 : Atomic s (CAS (Val v0) (Val v1) (Val v2)).
+Instance cmpxchg_atomic s v0 v1 v2 : Atomic s (CmpXchg (Val v0) (Val v1) (Val v2)).
 Proof. solve_atomic. Qed.
 Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
 Proof. solve_atomic. Qed.
@@ -375,46 +374,50 @@ Proof.
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_fail s E l q v' v1 v2 :
-  val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
-  {{{ ▷ l ↦{q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
+Lemma wp_cmpxchg_fail s E l q v' v1 v2 :
+  val_for_compare v' ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
+  {{{ ▷ l ↦{q} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+  {{{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }}}.
 Proof.
   iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+  rewrite bool_decide_false //.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
-Lemma twp_cas_fail s E l q v' v1 v2 :
-  val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
-  [[{ l ↦{q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  [[{ RET LitV (LitBool false); l ↦{q} v' }]].
+Lemma twp_cmpxchg_fail s E l q v' v1 v2 :
+  val_for_compare v' ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
+  [[{ l ↦{q} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+  [[{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  rewrite bool_decide_false //.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_suc s E l v1 v2 v' :
-  val_for_compare v' = val_for_compare v1 → vals_cas_compare_safe v' v1 →
-  {{{ ▷ l ↦ v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  {{{ RET LitV (LitBool true); l ↦ v2 }}}.
+Lemma wp_cmpxchg_suc s E l v1 v2 v' :
+  val_for_compare v' = val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
+  {{{ ▷ l ↦ v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+  {{{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }}}.
 Proof.
   iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+  rewrite bool_decide_true //.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
-Lemma twp_cas_suc s E l v1 v2 v' :
-  val_for_compare v' = val_for_compare v1 → vals_cas_compare_safe v' v1 →
-  [[{ l ↦ v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  [[{ RET LitV (LitBool true); l ↦ v2 }]].
+Lemma twp_cmpxchg_suc s E l v1 v2 v' :
+  val_for_compare v' = val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
+  [[{ l ↦ v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+  [[{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  rewrite bool_decide_true //.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
@@ -455,7 +458,7 @@ Qed.
 (* In the following, strong atomicity is required due to the fact that [e] must
 be able to make a head step for [Resolve e _ _] not to be (head) stuck. *)
 
-Lemma resolve_reducible e σ p v :
+Lemma resolve_reducible e σ (p : proph_id) v :
   Atomic StronglyAtomic e → reducible e σ →
   reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ.
 Proof.
@@ -468,10 +471,10 @@ Proof.
   simpl. constructor. by apply prim_step_to_val_is_head_step.
 Qed.
 
-Lemma step_resolve e p v σ1 κ e2 σ2 efs :
+Lemma step_resolve e vp vt σ1 κ e2 σ2 efs :
   Atomic StronglyAtomic e →
-  prim_step (Resolve e (Val p) (Val v)) σ1 κ e2 σ2 efs →
-  head_step (Resolve e (Val p) (Val v)) σ1 κ e2 σ2 efs.
+  prim_step (Resolve e (Val vp) (Val vt)) σ1 κ e2 σ2 efs →
+  head_step (Resolve e (Val vp) (Val vt)) σ1 κ e2 σ2 efs.
 Proof.
   intros A [Ks e1' e2' Hfill -> step]. simpl in *.
   induction Ks as [|K Ks _] using rev_ind.
@@ -485,13 +488,13 @@ Proof.
       assert (is_Some (to_val (fill (Ks ++ [K]) e2'))) as H.
       { apply (A σ1 _ κ σ2 efs). eapply Ectx_step with (K0 := Ks ++ [K]); done. }
       destruct H as [v H]. apply to_val_fill_some in H. by destruct H, Ks.
-    - assert (to_val (fill Ks e1') = Some p); first by rewrite -H1 //.
+    - assert (to_val (fill Ks e1') = Some vp); first by rewrite -H1 //.
       apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
-    - assert (to_val (fill Ks e1') = Some v); first by rewrite -H2 //.
+    - assert (to_val (fill Ks e1') = Some vt); first by rewrite -H2 //.
       apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
 Qed.
 
-Lemma wp_resolve s E e Φ p v pvs :
+Lemma wp_resolve s E e Φ (p : proph_id) v (pvs : list (val * val)) :
   Atomic StronglyAtomic e →
   to_val e = None →
   proph p pvs -∗
@@ -519,7 +522,8 @@ Proof.
     iMod "HΦ". iModIntro. by iApply "HΦ".
 Qed.
 
-Lemma wp_resolve_proph s E p pvs v :
+(** Lemmas for some particular expression inside the [Resolve]. *)
+Lemma wp_resolve_proph s E (p : proph_id) (pvs : list (val * val)) v :
   {{{ proph p pvs }}}
     ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
   {{{ pvs', RET (LitV LitUnit); ⌜pvs = (LitV LitUnit, v)::pvs'⌝ ∗ proph p pvs' }}}.
@@ -529,6 +533,32 @@ Proof.
   iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
 Qed.
 
+Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
+  vals_cmpxchg_compare_safe v1 v1 →
+  {{{ proph p pvs ∗ ▷ l ↦ v1 }}}
+    Resolve (CmpXchg #l v1 v2) #p v @ s; E
+  {{{ RET (v1, #true) ; ∃ pvs', ⌜pvs = ((v1, #true)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦ v2 }}}.
+Proof.
+  iIntros (Hcmp Φ) "[Hp Hl] HΦ".
+  iApply (wp_resolve with "Hp"); first done.
+  assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
+  iApply (wp_cmpxchg_suc with "Hl"); [done..|]. iIntros "!> Hl".
+  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
+Qed.
+
+Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
+  val_for_compare v' ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
+  {{{ proph p pvs ∗ ▷ l ↦{q} v' }}}
+    Resolve (CmpXchg #l v1 v2) #p v @ s; E
+  {{{ RET (v', #false) ; ∃ pvs', ⌜pvs = ((v', #false)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{q} v' }}}.
+Proof.
+  iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
+  iApply (wp_resolve with "Hp"); first done.
+  iApply (wp_cmpxchg_fail with "Hl"); [done..|]. iIntros "!> Hl".
+  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
+Qed.
+
+(** Array lemmas *)
 Lemma wp_allocN_vec s E v n :
   0 < n →
   {{{ True }}}
@@ -572,54 +602,54 @@ Proof.
   eexists. by apply vlookup_lookup.
 Qed.
 
-Lemma wp_cas_suc_offset s E l off vs v' v1 v2 :
+Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
   vs !! off = Some v' →
   val_for_compare v' = val_for_compare v1 →
-  vals_cas_compare_safe v' v1 →
+  vals_cmpxchg_compare_safe v' v1 →
   {{{ ▷ l ↦∗ vs }}}
-    CAS #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET #true; l ↦∗ <[off:=v2]> vs }}}.
+    CmpXchg #(l +â‚— off) v1 v2 @ s; E
+  {{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
 Proof.
   iIntros (Hlookup ?? Φ) "Hl HΦ".
   iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
-  iApply (wp_cas_suc with "Hl1"); [done..|].
+  iApply (wp_cmpxchg_suc with "Hl1"); [done..|].
   iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
 Qed.
 
-Lemma wp_cas_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
+Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
   val_for_compare (vs !!! off) = val_for_compare v1 →
-  vals_cas_compare_safe (vs !!! off) v1 →
+  vals_cmpxchg_compare_safe (vs !!! off) v1 →
   {{{ ▷ l ↦∗ vs }}}
-    CAS #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET #true; l ↦∗ vinsert off v2 vs }}}.
+    CmpXchg #(l +â‚— off) v1 v2 @ s; E
+  {{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}.
 Proof.
-  intros. setoid_rewrite vec_to_list_insert. eapply wp_cas_suc_offset=> //.
+  intros. setoid_rewrite vec_to_list_insert. eapply wp_cmpxchg_suc_offset=> //.
   by apply vlookup_lookup.
 Qed.
 
-Lemma wp_cas_fail_offset s E l off vs v0 v1 v2 :
+Lemma wp_cmpxchg_fail_offset s E l off vs v0 v1 v2 :
   vs !! off = Some v0 →
   val_for_compare v0 ≠ val_for_compare v1 →
-  vals_cas_compare_safe v0 v1 →
+  vals_cmpxchg_compare_safe v0 v1 →
   {{{ ▷ l ↦∗ vs }}}
-    CAS #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET #false; l ↦∗ vs }}}.
+    CmpXchg #(l +â‚— off) v1 v2 @ s; E
+  {{{ RET (v0, #false); l ↦∗ vs }}}.
 Proof.
   iIntros (Hlookup HNEq Hcmp Φ) ">Hl HΦ".
   iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
-  iApply (wp_cas_fail with "Hl1"); first done.
+  iApply (wp_cmpxchg_fail with "Hl1"); first done.
   { destruct Hcmp; by [ left | right ]. }
   iIntros "!> Hl1". iApply "HΦ". iDestruct ("Hl2" $! v0) as "Hl2".
   rewrite list_insert_id; last done. iApply "Hl2". iApply "Hl1".
 Qed.
 
-Lemma wp_cas_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
+Lemma wp_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
   val_for_compare (vs !!! off) ≠ val_for_compare v1 →
-  vals_cas_compare_safe (vs !!! off) v1 →
+  vals_cmpxchg_compare_safe (vs !!! off) v1 →
   {{{ ▷ l ↦∗ vs }}}
-    CAS #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET #false; l ↦∗ vs }}}.
-Proof. intros. eapply wp_cas_fail_offset=> //. by apply vlookup_lookup. Qed.
+    CmpXchg #(l +â‚— off) v1 v2 @ s; E
+  {{{ RET (vs !!! off, #false); l ↦∗ vs }}}.
+Proof. intros. eapply wp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
 
 Lemma wp_faa_offset s E l off vs (i1 i2 : Z) :
   vs !! off = Some #i1 →
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 0eba40f483149f7c4ecea6fb00518951328cb870..9df37184bacf13d0a4d26fa7f33a4967e6d467ef 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -14,7 +14,7 @@ Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
      is_closed_expr X e
   | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2 =>
      is_closed_expr X e1 && is_closed_expr X e2
-  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 | Resolve e0 e1 e2 =>
+  | If e0 e1 e2 | Case e0 e1 e2 | CmpXchg e0 e1 e2 | Resolve e0 e1 e2 =>
      is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2
   | NewProph => true
   end
@@ -135,6 +135,7 @@ Proof.
   - unfold un_op_eval in *. repeat case_match; naive_solver.
   - eapply bin_op_eval_closed; eauto; naive_solver.
   - by apply heap_closed_alloc.
+  - case_match; try apply map_Forall_insert_2; by naive_solver.
 Qed.
 
 (* Parallel substitution with maps of values indexed by strings *)
@@ -169,7 +170,7 @@ Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
   | AllocN e1 e2 => AllocN (subst_map vs e1) (subst_map vs e2)
   | Load e => Load (subst_map vs e)
   | Store e1 e2 => Store (subst_map vs e1) (subst_map vs e2)
-  | CAS e0 e1 e2 => CAS (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
+  | CmpXchg e0 e1 e2 => CmpXchg (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
   | FAA e1 e2 => FAA (subst_map vs e1) (subst_map vs e2)
   | NewProph => NewProph
   | Resolve e0 e1 e2 => Resolve (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 204ec38ab76de2a755935bfdb13ef8a68350bb96..07e5df43260a4ac277bf6ecb0b51b9d5b97c54db 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -25,6 +25,8 @@ Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing).
 Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing).
 Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
 Notation Alloc e := (AllocN (Val $ LitV $ LitInt 1) e) (only parsing).
+(** Compare-and-set (CAS) returns just a boolean indicating success or failure. *)
+Notation CAS l e1 e2 := (Snd (CmpXchg l e1 e2)) (only parsing).
 
 (* Skip should be atomic, we sometimes open invariants around
    it. Hence, we need to explicitly use LamV instead of e.g., Seq. *)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index fcfb38bee6cd80e33ece13dc6a48919fbf0e7aab..fae67297290d3f88d0692d0e58fc00218f31e31d 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -182,8 +182,8 @@ Lemma tac_wp_allocN Δ Δ' s E j K v n Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (array l (replicate (Z.to_nat n) v))) Δ' = Some Δ'' ∧
-    envs_entails Δ'' (WP fill K (Val $ LitV l) @ s; E {{ Φ }})) →
-  envs_entails Δ (WP fill K (AllocN #n v) @ s; E {{ Φ }}).
+    envs_entails Δ'' (WP fill K (Val $ LitV $ LitLoc l) @ s; E {{ Φ }})) →
+  envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ? ? HΔ.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_allocN.
@@ -196,8 +196,8 @@ Lemma tac_twp_allocN Δ s E j K v n Φ :
   (∀ l, ∃ Δ',
     envs_app false (Esnoc Enil j (array l (replicate (Z.to_nat n) v))) Δ
     = Some Δ' ∧
-    envs_entails Δ' (WP fill K (Val $ LitV l) @ s; E [{ Φ }])) →
-  envs_entails Δ (WP fill K (AllocN #n v) @ s; E [{ Φ }]).
+    envs_entails Δ' (WP fill K (Val $ LitV $ LitLoc l) @ s; E [{ Φ }])) →
+  envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq=> ? HΔ.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_allocN.
@@ -211,7 +211,7 @@ Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
     envs_entails Δ'' (WP fill K (Val $ LitV l) @ s; E {{ Φ }})) →
-  envs_entails Δ (WP fill K (Alloc v) @ s; E {{ Φ }}).
+  envs_entails Δ (WP fill K (Alloc (Val v)) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ? HΔ.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
@@ -222,8 +222,8 @@ Qed.
 Lemma tac_twp_alloc Δ s E j K v Φ :
   (∀ l, ∃ Δ',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ = Some Δ' ∧
-    envs_entails Δ' (WP fill K (Val $ LitV l) @ s; E [{ Φ }])) →
-  envs_entails Δ (WP fill K (Alloc v) @ s; E [{ Φ }]).
+    envs_entails Δ' (WP fill K (Val $ LitV $ LitLoc l) @ s; E [{ Φ }])) →
+  envs_entails Δ (WP fill K (Alloc (Val v)) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq=> HΔ.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc.
@@ -278,97 +278,97 @@ Proof.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ :
+Lemma tac_wp_cmpxchg Δ Δ' Δ'' s E i K l v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  vals_cas_compare_safe v v1 →
+  vals_cmpxchg_compare_safe v v1 →
   (val_for_compare v = val_for_compare v1 →
-   envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }})) →
+   envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }})) →
   (val_for_compare v ≠ val_for_compare v1 →
-   envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }})) →
-  envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
+   envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }})) →
+  envs_entails Δ (WP fill K (CmpXchg (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ???? Hsuc Hfail.
   destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
   - rewrite -wp_bind. eapply wand_apply.
-    { eapply wp_cas_suc; eauto. }
+    { eapply wp_cmpxchg_suc; eauto. }
     rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
     apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
   - rewrite -wp_bind. eapply wand_apply.
-    { eapply wp_cas_fail; eauto. }
+    { eapply wp_cmpxchg_fail; eauto. }
     rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl.
     apply later_mono, sep_mono_r. apply wand_mono; auto.
 Qed.
-Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 Φ :
+Lemma tac_twp_cmpxchg Δ Δ' s E i K l v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
-  vals_cas_compare_safe v v1 →
+  vals_cmpxchg_compare_safe v v1 →
   (val_for_compare v = val_for_compare v1 →
-   envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }])) →
+   envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }])) →
   (val_for_compare v ≠ val_for_compare v1 →
-   envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }])) →
-  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
+   envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }])) →
+  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq=> ??? Hsuc Hfail.
   destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
   - rewrite -twp_bind. eapply wand_apply.
-    { eapply twp_cas_suc; eauto. }
+    { eapply twp_cmpxchg_suc; eauto. }
     rewrite /= {1}envs_simple_replace_sound //; simpl.
     apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
   - rewrite -twp_bind. eapply wand_apply.
-    { eapply twp_cas_fail; eauto. }
+    { eapply twp_cmpxchg_fail; eauto. }
     rewrite /= {1}envs_lookup_split //; simpl.
     apply sep_mono_r. apply wand_mono; auto.
 Qed.
 
-Lemma tac_wp_cas_fail Δ Δ' s E i K l q v v1 v2 Φ :
+Lemma tac_wp_cmpxchg_fail Δ Δ' s E i K l q v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  val_for_compare v ≠ val_for_compare v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
+  val_for_compare v ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v v1 →
+  envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ?????.
-  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_cmpxchg_fail.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
-Lemma tac_twp_cas_fail Δ s E i K l q v v1 v2 Φ :
+Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦{q} v)%I →
-  val_for_compare v ≠ val_for_compare v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }]) →
-  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
+  val_for_compare v ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v v1 →
+  envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq. intros. rewrite -twp_bind.
-  eapply wand_apply; first exact: twp_cas_fail.
+  eapply wand_apply; first exact: twp_cmpxchg_fail.
   rewrite envs_lookup_split //=. by do 2 f_equiv.
 Qed.
 
-Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
+Lemma tac_wp_cmpxchg_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  val_for_compare v = val_for_compare v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
+  val_for_compare v = val_for_compare v1 → vals_cmpxchg_compare_safe v v1 →
+  envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ??????; subst.
   rewrite -wp_bind. eapply wand_apply.
-  { eapply wp_cas_suc; eauto. }
+  { eapply wp_cmpxchg_suc; eauto. }
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
-Lemma tac_twp_cas_suc Δ Δ' s E i K l v v1 v2 Φ :
+Lemma tac_twp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
-  val_for_compare v = val_for_compare v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }]) →
-  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
+  val_for_compare v = val_for_compare v1 → vals_cmpxchg_compare_safe v v1 →
+  envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq=>?????; subst.
   rewrite -twp_bind. eapply wand_apply.
-  { eapply twp_cas_suc; eauto. }
+  { eapply twp_cmpxchg_suc; eauto. }
   rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
@@ -530,104 +530,104 @@ Tactic Notation "wp_store" :=
   | _ => fail "wp_store: not a 'wp'"
   end.
 
-Ltac solve_vals_cas_compare_safe :=
-  (* The first branch is for when we have [vals_cas_compare_safe] in the context.
+Ltac solve_vals_cmpxchg_compare_safe :=
+  (* The first branch is for when we have [vals_cmpxchg_compare_safe] in the context.
      The other two branches are for when either one of the branches reduces to
      [True] or we have it in the context. *)
   fast_done || (left; fast_done) || (right; fast_done).
 
-Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2) :=
+Tactic Notation "wp_cmpxchg" "as" simple_intropattern(H1) "|" simple_intropattern(H2) :=
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-    iAssumptionCore || fail "wp_cas: cannot find" l "↦ ?" in
+    iAssumptionCore || fail "wp_cmpxchg: cannot find" l "↦ ?" in
   wp_pures;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas _ _ _ _ _ _ K))
-      |fail 1 "wp_cas: cannot find 'CAS' in" e];
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cmpxchg _ _ _ _ _ _ K))
+      |fail 1 "wp_cmpxchg: cannot find 'CmpXchg' in" e];
     [iSolveTC
     |solve_mapsto ()
     |pm_reflexivity
-    |try solve_vals_cas_compare_safe
+    |try solve_vals_cmpxchg_compare_safe
     |intros H1; wp_finish
     |intros H2; wp_finish]
   | |- envs_entails _ (twp ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas _ _ _ _ _ K))
-      |fail 1 "wp_cas: cannot find 'CAS' in" e];
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cmpxchg _ _ _ _ _ K))
+      |fail 1 "wp_cmpxchg: cannot find 'CmpXchg' in" e];
     [solve_mapsto ()
     |pm_reflexivity
-    |try solve_vals_cas_compare_safe
+    |try solve_vals_cmpxchg_compare_safe
     |intros H1; wp_finish
     |intros H2; wp_finish]
-  | _ => fail "wp_cas: not a 'wp'"
+  | _ => fail "wp_cmpxchg: not a 'wp'"
   end.
 
-Tactic Notation "wp_cas_fail" :=
+Tactic Notation "wp_cmpxchg_fail" :=
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-    iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" in
+    iAssumptionCore || fail "wp_cmpxchg_fail: cannot find" l "↦ ?" in
   wp_pures;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_fail _ _ _ _ _ K))
-      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cmpxchg_fail _ _ _ _ _ K))
+      |fail 1 "wp_cmpxchg_fail: cannot find 'CmpXchg' in" e];
     [iSolveTC
     |solve_mapsto ()
     |try (simpl; congruence) (* value inequality *)
-    |try solve_vals_cas_compare_safe
+    |try solve_vals_cmpxchg_compare_safe
     |wp_finish]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_fail _ _ _ _ K))
-      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cmpxchg_fail _ _ _ _ K))
+      |fail 1 "wp_cmpxchg_fail: cannot find 'CmpXchg' in" e];
     [solve_mapsto ()
     |try (simpl; congruence) (* value inequality *)
-    |try solve_vals_cas_compare_safe
+    |try solve_vals_cmpxchg_compare_safe
     |wp_finish]
-  | _ => fail "wp_cas_fail: not a 'wp'"
+  | _ => fail "wp_cmpxchg_fail: not a 'wp'"
   end.
 
-Tactic Notation "wp_cas_suc" :=
+Tactic Notation "wp_cmpxchg_suc" :=
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
+    iAssumptionCore || fail "wp_cmpxchg_suc: cannot find" l "↦ ?" in
   wp_pures;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_suc _ _ _ _ _ _ K))
-      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cmpxchg_suc _ _ _ _ _ _ K))
+      |fail 1 "wp_cmpxchg_suc: cannot find 'CmpXchg' in" e];
     [iSolveTC
     |solve_mapsto ()
     |pm_reflexivity
     |try (simpl; congruence) (* value equality *)
-    |try solve_vals_cas_compare_safe
+    |try solve_vals_cmpxchg_compare_safe
     |wp_finish]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_suc _ _ _ _ _ K))
-      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cmpxchg_suc _ _ _ _ _ K))
+      |fail 1 "wp_cmpxchg_suc: cannot find 'CmpXchg' in" e];
     [solve_mapsto ()
     |pm_reflexivity
     |try (simpl; congruence) (* value equality *)
-    |try solve_vals_cas_compare_safe
+    |try solve_vals_cmpxchg_compare_safe
     |wp_finish]
-  | _ => fail "wp_cas_suc: not a 'wp'"
+  | _ => fail "wp_cmpxchg_suc: not a 'wp'"
   end.
 
 Tactic Notation "wp_faa" :=
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
+    iAssumptionCore || fail "wp_faa: cannot find" l "↦ ?" in
   wp_pures;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_faa _ _ _ _ _ _ K))
-      |fail 1 "wp_faa: cannot find 'CAS' in" e];
+      |fail 1 "wp_faa: cannot find 'FAA' in" e];
     [iSolveTC
     |solve_mapsto ()
     |pm_reflexivity
@@ -635,7 +635,7 @@ Tactic Notation "wp_faa" :=
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_twp_faa _ _ _ _ _ K))
-      |fail 1 "wp_faa: cannot find 'CAS' in" e];
+      |fail 1 "wp_faa: cannot find 'FAA' in" e];
     [solve_mapsto ()
     |pm_reflexivity
     |wp_finish]
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 6ea6feb75b0d4041d54b3f70c8612c7858994dd3..368f202fe40127e70e64b10c6bf0bf755bef4cab 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -35,9 +35,9 @@ Ltac reshape_expr e tac :=
     | Load ?e                         => add_item LoadCtx vs K e
     | Store ?e (Val ?v)               => add_item (StoreLCtx v) vs K e
     | Store ?e1 ?e2                   => add_item (StoreRCtx e1) vs K e2
-    | CAS ?e0 (Val ?v1) (Val ?v2)     => add_item (CasLCtx v1 v2) vs K e0
-    | CAS ?e0 ?e1 (Val ?v2)           => add_item (CasMCtx e0 v2) vs K e1
-    | CAS ?e0 ?e1 ?e2                 => add_item (CasRCtx e0 e1) vs K e2
+    | CmpXchg ?e0 (Val ?v1) (Val ?v2) => add_item (CmpXchgLCtx v1 v2) vs K e0
+    | CmpXchg ?e0 ?e1 (Val ?v2)       => add_item (CmpXchgMCtx e0 v2) vs K e1
+    | CmpXchg ?e0 ?e1 ?e2             => add_item (CmpXchgRCtx e0 e1) vs K e2
     | FAA ?e (Val ?v)                 => add_item (FaaLCtx v) vs K e
     | FAA ?e1 ?e2                     => add_item (FaaRCtx e1) vs K e2
     | Resolve ?ex (Val ?v1) (Val ?v2) => go K ((v1,v2) :: vs) ex