From 12bec4d549d8f344668306e3573dd3b983ce6f5b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 20 Jun 2019 23:24:13 +0200
Subject: [PATCH] rename CompareExchange to CmpXchg

This is the name used by x86 (CMPXCHG) and LLVM.  Also reorder the result (value
first, boolean second) for consistency with LLVM, because why not.
---
 tests/heap_lang.ref                  |   8 +-
 tests/heap_lang.v                    |  18 ++--
 tests/heap_lang_proph.v              |   9 +-
 tests/ipm_paper.v                    |   6 +-
 tests/one_shot.v                     |   6 +-
 theories/heap_lang/lang.v            |  60 ++++++-------
 theories/heap_lang/lib/atomic_heap.v |  46 +++++++---
 theories/heap_lang/lib/counter.v     |  12 +--
 theories/heap_lang/lib/increment.v   |   6 +-
 theories/heap_lang/lib/spin_lock.v   |   6 +-
 theories/heap_lang/lib/ticket_lock.v |   6 +-
 theories/heap_lang/lifting.v         |  96 ++++++++++----------
 theories/heap_lang/metatheory.v      |   4 +-
 theories/heap_lang/notation.v        |   3 +-
 theories/heap_lang/proofmode.v       | 128 +++++++++++++--------------
 theories/heap_lang/tactics.v         |   9 +-
 16 files changed, 221 insertions(+), 202 deletions(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index cd0bad54e..eaaa3c963 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -40,7 +40,7 @@
   ============================
   _ : ▷ l ↦ #0
   --------------------------------------∗
-  WP CompareExchange #l #0 #1 {{ _, l ↦ #1 }}
+  WP CmpXchg #l #0 #1 {{ _, l ↦ #1 }}
   
 1 subgoal
   
@@ -144,9 +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 'CompareExchange' 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 fe19053fb..df044f7f6 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", CompareExchange "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 CompareExchange #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 7eb5a86b7..b7022b445 100644
--- a/tests/heap_lang_proph.v
+++ b/tests/heap_lang_proph.v
@@ -11,11 +11,14 @@ Section tests.
   Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
     l ↦ #n -∗
     proph p vs -∗
-    WP Resolve (CompareExchange #l #n (#n + #1)) #p v @ E
-      {{ v, ⌜v = (#true, #n)%V⌝ ∗ ∃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) }}%I.
   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)) :
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index d961c559b..79ec0d82a 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -222,17 +222,17 @@ 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 (CompareExchange _ _ _). 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_pures. rewrite {3}/C; eauto 10.
-    - wp_cas_fail; first (intros [=]; abstract omega).
+    - wp_cmpxchg_fail; first (intros [=]; abstract omega).
       iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
       wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
   Qed.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 2c93e917b..01159f1a7 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. wp_bind (CompareExchange _ _ _).
+  - 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. iModIntro. iSplitL; last (wp_pures; by eauto).
+      wp_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
       iNext; iRight; iExists n; by iFrame.
-    + wp_cas_fail. iModIntro. iSplitL; last (wp_pures; by eauto).
+    + 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 4a9272d89..cb8303086 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,7 +97,7 @@ Inductive expr :=
   | AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
-  | CompareExchange (e0 : expr) (e1 : expr) (e2 : expr)
+  | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr)
   | FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *)
   (* Prophecy *)
   | NewProph
@@ -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'))
-     | CompareExchange e0 e1 e2, CompareExchange 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]
-     | CompareExchange 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] => CompareExchange (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)
-  | CompareExchangeLCtx (v1 : val) (v2 : val)
-  | CompareExchangeMCtx (e0 : expr) (v2 : val)
-  | CompareExchangeRCtx (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
-  | CompareExchangeLCtx v1 v2 => CompareExchange e (Val v1) (Val v2)
-  | CompareExchangeMCtx e0 v2 => CompareExchange e0 e (Val v2)
-  | CompareExchangeRCtx e0 e1 => CompareExchange 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)
-  | CompareExchange e0 e1 e2 => CompareExchange (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,7 +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 [CAS]! *)
+    (* 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
@@ -634,14 +634,14 @@ Inductive head_step : expr → state → list observation → expr → state →
                []
                (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
                []
-  | CompareExchangeS l v1 v2 vl σ b :
-     vals_cas_compare_safe vl v1 →
+  | CmpXchgS l v1 v2 vl σ b :
+     vals_cmpxchg_compare_safe vl v1 →
      σ.(heap) !! l = Some vl →
      (* Crucially, this compares the same way as [EqOp]! *)
      b = bool_decide (val_for_compare vl = val_for_compare v1) →
-     head_step (CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
+     head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
                []
-               (Val $ PairV (LitV $ LitBool b) vl) (if b then state_upd_heap <[l:=v2]> σ else σ)
+               (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 2b5e28cce..fc059f5c9 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 -- *)
@@ -34,11 +34,11 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   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. *)
-  cas_spec (l : loc) (w1 w2 : val) :
+  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 _ {_}.
 
@@ -56,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".
@@ -67,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 Σ}.
@@ -97,18 +115,18 @@ 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_pures. wp_bind (CompareExchange _ _ _).
+    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];
-    iMod ("Hclose" with "H↦") as "HΦ"; iModIntro; by wp_pures.
+      [wp_cmpxchg_suc|wp_cmpxchg_fail];
+    iMod ("Hclose" with "H↦") as "HΦ"; done.
   Qed.
 End proof.
 
@@ -118,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 18a371188..4b7058988 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -50,20 +50,20 @@ 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 (CompareExchange _ _ _).
+    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_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_pures. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
       rewrite {3}/mcounter; eauto 10.
@@ -129,15 +129,15 @@ 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 (CompareExchange _ _ _).
+    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_pures. by iApply "HΦ".
-    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
+    - wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]).
       iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
       wp_pures. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
   Qed.
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index 1fbdea446..00065aa8d 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -26,11 +26,11 @@ 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 (CompareExchange _ _ _)%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Φ".
+    - wp_cmpxchg_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
       iModIntro. wp_pures. done.
-    - wp_cas_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
+    - 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 36ed310db..3370bdcc2 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -61,10 +61,10 @@ 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. wp_bind (CompareExchange _ _ _). iInv N as ([]) "[Hl HR]".
-    - wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
+    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_cas_suc. iDestruct "HR" as "[Hγ HR]".
+    - wp_cmpxchg_suc. iDestruct "HR" as "[Hγ HR]".
       iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
       rewrite /locked. wp_pures. by iApply ("HΦ" $! true with "[$Hγ $HR]").
   Qed.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 7042cbace..5600f18d9 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 (CompareExchange _ _ _).
+    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,14 +119,14 @@ 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_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_pures. by iApply "IH"; auto.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index a060eb6ff..9e5e2098c 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -56,7 +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 (CompareExchange _ _ _) _ _ _ _ _) => eapply CompareExchangeS : 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.
@@ -77,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 (CompareExchange (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.
@@ -374,10 +374,10 @@ 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' }}} CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  {{{ RET (#false, v'); 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 (v', #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 %?.
@@ -385,10 +385,10 @@ Proof.
   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' }]] CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  [[{ RET (#false, v'); 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 (v', #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 %?.
@@ -397,10 +397,10 @@ Proof.
   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' }}} CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  {{{ RET (#true, v'); 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 (v', #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 %?.
@@ -409,10 +409,10 @@ Proof.
   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' }]] CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  [[{ RET (#true, v'); 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 (v', #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 %?.
@@ -533,28 +533,28 @@ Proof.
   iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
 Qed.
 
-Lemma wp_resolve_cas_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
-  vals_cas_compare_safe v1 v1 →
+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 (CompareExchange #l v1 v2) #p v @ s; E
-  {{{ RET (#true, v1) ; ∃ pvs', ⌜pvs = ((#true, v1)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦ v2 }}}.
+    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_cas_suc with "Hl"); [done..|]. iIntros "!> Hl".
+  iApply (wp_cmpxchg_suc with "Hl"); [done..|]. iIntros "!> Hl".
   iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
 Qed.
 
-Lemma wp_resolve_cas_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_cas_compare_safe v' v1 →
+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 (CompareExchange #l v1 v2) #p v @ s; E
-  {{{ RET (#false, v') ; ∃ pvs', ⌜pvs = ((#false, v')%V, v)::pvs'⌝ ∗ 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_cas_fail with "Hl"); [done..|]. iIntros "!> Hl".
+  iApply (wp_cmpxchg_fail with "Hl"); [done..|]. iIntros "!> Hl".
   iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
 Qed.
 
@@ -602,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 }}}
-    CompareExchange #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET (#true, v'); 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 }}}
-    CompareExchange #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET (#true, vs !!! off); 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 }}}
-    CompareExchange #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET (#false, v0); 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 }}}
-    CompareExchange #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET (#false, vs !!! off); 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 a4b667f6b..9df37184b 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 | CompareExchange 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
@@ -170,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)
-  | CompareExchange e0 e1 e2 => CompareExchange (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 f926a7e85..861b4a17d 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -25,7 +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).
-Notation CAS l e1 e2 := (Fst (CompareExchange l e1 e2)) (only parsing).
+(** Compare-and-set (CAS) retursn 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 77acaed17..2eab8e069 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -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 (#true, v)) @ s; E {{ Φ }})) →
+   envs_entails Δ'' (WP fill K (Val (v, #true)) @ s; E {{ Φ }})) →
   (val_for_compare v ≠ val_for_compare v1 →
-   envs_entails Δ' (WP fill K (Val (#false, v)) @ s; E {{ Φ }})) →
-  envs_entails Δ (WP fill K (CompareExchange (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
+   envs_entails Δ' (WP fill K (Val (v, #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 (#true, v)) @ s; E [{ Φ }])) →
+   envs_entails Δ' (WP fill K (Val (v, #true)) @ s; E [{ Φ }])) →
   (val_for_compare v ≠ val_for_compare v1 →
-   envs_entails Δ (WP fill K (Val (#false, v)) @ s; E [{ Φ }])) →
-  envs_entails Δ (WP fill K (CompareExchange (LitV l) v1 v2) @ s; E [{ Φ }]).
+   envs_entails Δ (WP fill K (Val (v, #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 (#false, v)) @ s; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CompareExchange (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 (v, #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 (#false, v)) @ s; E [{ Φ }]) →
-  envs_entails Δ (WP fill K (CompareExchange (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 (v, #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 (#true, v)) @ s; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CompareExchange (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 (v, #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 (#true, v)) @ s; E [{ Φ }]) →
-  envs_entails Δ (WP fill K (CompareExchange (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 (v, #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,98 +530,98 @@ 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 'CompareExchange' 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 'CompareExchange' 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 'CompareExchange' 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 'CompareExchange' 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 'CompareExchange' 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 'CompareExchange' 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) =>
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 041e36f32..368f202fe 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -35,12 +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
-    | CompareExchange ?e0 (Val ?v1) (Val ?v2)
-                                      => add_item (CompareExchangeLCtx v1 v2) vs K e0
-    | CompareExchange ?e0 ?e1 (Val ?v2)
-                                      => add_item (CompareExchangeMCtx e0 v2) vs K e1
-    | CompareExchange ?e0 ?e1 ?e2
-                                      => add_item (CompareExchangeRCtx 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
-- 
GitLab