diff --git a/_CoqProject b/_CoqProject
index dcc37e6b710e4dc07435ecc7e8c4885a340c8c0c..1cf8c32397c3167d860d5ff6599395512a7c0edc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -109,4 +109,3 @@ theories/logatom/conditional_increment/spec.v
 theories/logatom/conditional_increment/cinc.v
 theories/logatom/rdcss/rdcss.v
 theories/logatom/rdcss/spec.v
-theories/logatom/rdcss/lib/gc.v
diff --git a/theories/logatom/lib/gc.v b/theories/logatom/lib/gc.v
index ecd69be06c92ce1a72d8ce7a720dd3dfcbcaa106..9ed34a0be5ad0719889006d23b14fe4b47a3425f 100644
--- a/theories/logatom/lib/gc.v
+++ b/theories/logatom/lib/gc.v
@@ -11,7 +11,7 @@ Definition gc_mapUR : ucmraT := gmapUR loc $ optionR $ exclR $ valO.
 
 Definition to_gc_map (gcm: gmap loc val) : gc_mapUR := (λ v : val, Excl' v) <$> gcm.
 
-Class gcG  (Σ : gFunctors) := Gc_mapG {
+Class gcG  (Σ : gFunctors) := GcG {
   gc_inG :> inG Σ (authR (gc_mapUR));
   gc_name : gname
 }.
@@ -111,11 +111,25 @@ Section to_gc_map.
   Qed.
 End to_gc_map.
 
+Lemma gc_init `{!invG Σ, !heapG Σ, !gcPreG Σ} E:
+  (|==> ∃ _ : gcG Σ, |={E}=> gc_inv)%I.
+Proof.
+  iMod (own_alloc (● (to_gc_map ∅))) as (γ) "H●".
+  { rewrite auth_auth_valid. exact: to_gc_map_valid. }
+  iModIntro.
+  iExists (GcG Σ _ γ).
+  iAssert (gc_inv_P (gG := GcG Σ _ γ)) with "[H●]" as "P". 
+  {
+    iExists _. iFrame.
+    by iApply big_sepM_empty.
+  }
+  iMod ((inv_alloc gcN E gc_inv_P) with "P") as "#InvGC".
+  iModIntro. iFrame "#".
+Qed.
+
 Section gc.
   Context `{!invG Σ, !heapG Σ, !gcG Σ}.
 
-  (* FIXME: still needs a constructor. *)
-
   Global Instance is_gc_loc_persistent (l: loc): Persistent (is_gc_loc l).
   Proof. rewrite /is_gc_loc. apply _. Qed.
 
diff --git a/theories/logatom/rdcss/lib/gc.v b/theories/logatom/rdcss/lib/gc.v
deleted file mode 100644
index 85365ba960f16cfff1177f810530179c670e3482..0000000000000000000000000000000000000000
--- a/theories/logatom/rdcss/lib/gc.v
+++ /dev/null
@@ -1,245 +0,0 @@
-From iris.algebra Require Import auth excl gmap.
-From iris.base_logic.lib Require Export own invariants.
-From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Export lang locations lifting.
-Set Default Proof Using "Type".
-Import uPred.
-
-Definition gcN: namespace := nroot .@ "gc".
-
-Definition gc_mapUR : ucmraT := gmapUR loc $ optionR $ exclR $ valC.
-
-Definition to_gc_map (gcm: gmap loc val) : gc_mapUR := (λ v : val, Excl' v) <$> gcm.
-
-Class gcG  (Σ : gFunctors) := GcG {
-  gc_inG :> inG Σ (authR (gc_mapUR));
-  gc_name : gname
-}.
-
-Arguments gc_name {_} _ : assert.
-
-Class gcPreG (Σ : gFunctors) := {
-  gc_preG_inG :> inG Σ (authR (gc_mapUR))
-}.
-
-Definition gcΣ : gFunctors :=
-  #[ GFunctor (authR (gc_mapUR)) ].
-
-Instance subG_gcPreG {Σ} : subG gcΣ Σ → gcPreG Σ.
-Proof. solve_inG. Qed.
-
-Section defs.
-
-  Context `{!invG Σ, !heapG Σ, gG: gcG Σ}.
-
-  Definition gc_inv_P: iProp Σ := 
-    ((∃(gcm: gmap loc val), own (gc_name gG) (● to_gc_map gcm) ∗ ([∗ map] l ↦ v ∈ gcm, (l ↦ v)) ) )%I.
-
-  Definition gc_inv : iProp Σ := inv gcN gc_inv_P.
-
-  Definition gc_mapsto (l: loc) (v: val) : iProp Σ := own (gc_name gG) (◯ {[l := Excl' v]}).
-
-  Definition is_gc_loc (l: loc) : iProp Σ := own (gc_name gG) (◯ {[l := None]}).
-
-End defs.
-
-Section to_gc_map.
-
-  Lemma to_gc_map_valid gcm: ✓ to_gc_map gcm.
-  Proof. intros l. rewrite lookup_fmap. by case (gcm !! l). Qed.
-
-  Lemma to_gc_map_empty: to_gc_map ∅ = ∅.
-  Proof. by rewrite /to_gc_map fmap_empty. Qed.
-
-  Lemma to_gc_map_singleton l v: to_gc_map {[l := v]} = {[l :=  Excl' v]}.
-  Proof. by rewrite /to_gc_map fmap_insert fmap_empty. Qed.
-
-  Lemma to_gc_map_insert l v gcm:
-    to_gc_map (<[l := v]> gcm) = <[l := Excl' v]> (to_gc_map gcm).
-  Proof. by rewrite /to_gc_map fmap_insert. Qed.
-
-  Lemma to_gc_map_delete l gcm :
-    to_gc_map (delete l gcm) = delete l (to_gc_map gcm).
-  Proof. by rewrite /to_gc_map fmap_delete. Qed.
-
-  Lemma lookup_to_gc_map_None gcm l :
-    gcm !! l = None → to_gc_map gcm !! l = None.
-  Proof. by rewrite /to_gc_map lookup_fmap=> ->. Qed.
-
-  Lemma lookup_to_gc_map_Some gcm l v :
-    gcm !! l = Some v → to_gc_map gcm !! l = Some (Excl' v).
-  Proof. by rewrite /to_gc_map lookup_fmap=> ->. Qed.
-
-
-  Lemma lookup_to_gc_map_Some_2 gcm l w :
-    to_gc_map gcm !! l = Some w → ∃ v, gcm !! l = Some v.
-  Proof.
-    rewrite /to_gc_map lookup_fmap. rewrite fmap_Some.
-    intros (x & Hsome & Heq). eauto.
-  Qed.
-
-  Lemma lookup_to_gc_map_Some_3 gcm l w :
-    to_gc_map gcm !! l = Some (Excl' w) → gcm !! l = Some w.
-  Proof.
-    rewrite /to_gc_map lookup_fmap. rewrite fmap_Some.
-    intros (x & Hsome & Heq). by inversion Heq.
-  Qed.
-
-  Lemma excl_option_included (v: val) y:
-    ✓ y → Excl' v ≼ y → y = Excl' v.
-  Proof.
-    intros ? H. destruct y.
-    - apply Some_included_exclusive in H;[ | apply _ | done ].
-      setoid_rewrite leibniz_equiv_iff in H.
-      by rewrite H.
-    - apply is_Some_included in H.
-      + by inversion H.
-      + by eapply mk_is_Some.
-  Qed.
-
-  Lemma gc_map_singleton_included gcm l v :
-    {[l := Some (Excl v)]} ≼ to_gc_map gcm → gcm !! l = Some v.
-  Proof.
-    rewrite singleton_included.
-    setoid_rewrite Some_included_total.
-    intros (y & Hsome & Hincluded).
-    pose proof (lookup_valid_Some _ _ _ (to_gc_map_valid gcm) Hsome) as Hvalid.
-    pose proof (excl_option_included _ _ Hvalid Hincluded) as Heq.
-    rewrite Heq in Hsome.
-    apply lookup_to_gc_map_Some_3.
-    by setoid_rewrite leibniz_equiv_iff in Hsome.
-  Qed.
-End to_gc_map.
-
-Lemma gc_init `{!invG Σ, !heapG Σ, !gcPreG Σ} E:
-  (|==> ∃ _ : gcG Σ, |={E}=> gc_inv)%I.
-Proof.
-  iMod (own_alloc (● (to_gc_map ∅))) as (γ) "H●".
-  { rewrite auth_auth_valid. exact: to_gc_map_valid. }
-  iModIntro.
-  iExists (GcG Σ _ γ).
-  iAssert (gc_inv_P (gG := GcG Σ _ γ)) with "[H●]" as "P". 
-  {
-    iExists _. iFrame.
-    by iApply big_sepM_empty.
-  }
-  iMod ((inv_alloc gcN E gc_inv_P) with "P") as "#InvGC".
-  iModIntro. iFrame "#".
-Qed.
-
-Section gc.
-  Context `{!invG Σ, !heapG Σ, !gcG Σ}.
-
-  (* FIXME: still needs a constructor. *)
-
-  Global Instance is_gc_loc_persistent (l: loc): Persistent (is_gc_loc l).
-  Proof. rewrite /is_gc_loc. apply _. Qed.
-
-  Global Instance is_gc_loc_timeless (l: loc): Timeless (is_gc_loc l).
-  Proof. rewrite /is_gc_loc. apply _. Qed.
-
-  Global Instance gc_mapsto_timeless (l: loc) (v: val): Timeless (gc_mapsto l v).
-  Proof. rewrite /is_gc_loc. apply _. Qed.
-
-  Global Instance gc_inv_P_timeless: Timeless gc_inv_P.
-  Proof. rewrite /gc_inv_P. apply _. Qed.
-
-  Lemma make_gc l v E: ↑gcN ⊆ E → gc_inv -∗ l ↦ v ={E}=∗ gc_mapsto l v.
-  Proof.
-    iIntros (HN) "#Hinv Hl".
-    iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
-    iDestruct "P" as (gcm) "[H● HsepM]".
-    destruct (gcm !! l) as [v' | ] eqn: Hlookup.
-    - (* auth map contains l --> contradiction *)
-      iDestruct (big_sepM_lookup with "HsepM") as "Hl'"=>//.
-      by iDestruct (mapsto_valid_2 with "Hl Hl'") as %?.
-    - iMod (own_update with "H●") as "[H● H◯]".
-      {
-        apply lookup_to_gc_map_None in Hlookup.
-        apply (auth_update_alloc _ (to_gc_map (<[l := v]> gcm)) (to_gc_map ({[l := v]}))).
-        rewrite to_gc_map_insert to_gc_map_singleton.
-        pose proof (to_gc_map_valid gcm).
-        setoid_rewrite alloc_singleton_local_update=>//.
-      }
-      iMod ("Hclose" with "[H● HsepM Hl]"). 
-      + iExists _.
-        iDestruct (big_sepM_insert with "[HsepM Hl]") as "HsepM"=>//; iFrame. iFrame.
-      + iModIntro. by rewrite /gc_mapsto to_gc_map_singleton.
-  Qed.
-
-  Lemma gc_is_gc l v: gc_mapsto l v -∗ is_gc_loc l.
-  Proof.
-    iIntros "Hgc_l". rewrite /gc_mapsto.
-    assert (Excl' v = (Excl' v) â‹… None)%I as ->. { done. }
-    rewrite -op_singleton auth_frag_op own_op.
-    iDestruct "Hgc_l" as "[_ Hâ—¯_none]".
-    iFrame.
-  Qed.
-
-  Lemma is_gc_lookup_Some  l gcm: is_gc_loc l -∗ own (gc_name _) (● to_gc_map gcm) -∗ ⌜∃ v, gcm !! l = Some v⌝.
-    iIntros "Hgc_l Hâ—¯".
-    iCombine "Hâ—¯ Hgc_l" as "Hcomb".
-    iDestruct (own_valid with "Hcomb") as %Hvalid.
-    iPureIntro.
-    apply auth_both_valid in Hvalid as [Hincluded Hvalid]. 
-    setoid_rewrite singleton_included in Hincluded. 
-    destruct Hincluded as (y & Hsome & _).
-    eapply lookup_to_gc_map_Some_2.
-    by apply leibniz_equiv_iff in Hsome.
-  Qed.
-
-  Lemma gc_mapsto_lookup_Some l v gcm: gc_mapsto l v -∗ own (gc_name _) (● to_gc_map gcm) -∗ ⌜ gcm !! l = Some v ⌝.
-  Proof.
-    iIntros "Hgc_l H●".
-    iCombine "H● Hgc_l" as "Hcomb".
-    iDestruct (own_valid with "Hcomb") as %Hvalid.
-    iPureIntro.
-    apply auth_both_valid in Hvalid as [Hincluded Hvalid]. 
-    by apply gc_map_singleton_included.
-  Qed.
-
-  (** An accessor to make use of [gc_mapsto].
-    This opens the invariant *before* consuming [gc_mapsto] so that you can use
-    this before opening an atomic update that provides [gc_mapsto]!. *)
-  Lemma gc_access E:
-    ↑gcN ⊆ E →
-    gc_inv ={E, E ∖ ↑gcN}=∗ ∀ l v, gc_mapsto l v -∗
-      (l ↦ v ∗ (∀ w, l ↦ w ==∗ gc_mapsto l w ∗ |={E ∖ ↑gcN, E}=> True)).
-  Proof.
-    iIntros (HN) "#Hinv".
-    iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
-    iIntros "!>" (l v) "Hgc_l".
-    iDestruct "P" as (gcm) "[H● HsepM]".
-    iDestruct (gc_mapsto_lookup_Some with "Hgc_l H●") as %Hsome.
-    iDestruct (big_sepM_delete with "HsepM") as "[Hl HsepM]"=>//. 
-    iFrame. iIntros (w) "Hl".
-    iMod (own_update_2 with "H● Hgc_l") as "[H● H◯]".
-    { apply (auth_update _ _ (<[l := Excl' w]> (to_gc_map gcm)) {[l := Excl' w]}).
-      eapply singleton_local_update.
-      { by apply lookup_to_gc_map_Some in Hsome. }
-      by apply option_local_update, exclusive_local_update.
-    }
-    iDestruct (big_sepM_insert with "[Hl HsepM]") as "HsepM"; [ | iFrame | ].
-    { apply lookup_delete. }
-    rewrite insert_delete. rewrite <- to_gc_map_insert.
-    iModIntro. iFrame.
-    iMod ("Hclose" with "[H● HsepM]"); [ iExists _; by iFrame | by iModIntro].
-  Qed.   
-
-  Lemma is_gc_access l E: ↑gcN ⊆ E → gc_inv -∗ is_gc_loc l ={E, E ∖ ↑gcN}=∗ ∃ v, l ↦ v ∗ (l ↦ v ={E ∖ ↑gcN, E}=∗ ⌜True⌝).
-  Proof.
-    iIntros (HN) "#Hinv Hgc_l".
-    iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
-    iModIntro.
-    iDestruct "P" as (gcm) "[H● HsepM]".
-    iDestruct (is_gc_lookup_Some with "Hgc_l H●") as %Hsome.
-    destruct Hsome as [v Hsome].
-    iDestruct (big_sepM_lookup_acc with "HsepM") as "[Hl HsepM]"=>//. 
-    iExists _. iFrame.
-    iIntros "Hl".
-    iMod ("Hclose" with "[H● HsepM Hl]"); last done.
-    iExists _. iFrame.
-    by (iApply ("HsepM" with "Hl")).
-  Qed.
-
-End gc.
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 0904c759cf7527b075bcce0fe95ab878bbecea7a..602c59142fd7635c772d92b3b7646928ae9e8605 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -4,7 +4,6 @@ From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris_examples.logatom.rdcss Require Import spec.
-From iris_examples.logatom.rdcss Require Export gc.
 Import uPred bi List Decidable.
 Set Default Proof Using "Type".
 
@@ -43,7 +42,7 @@ Definition new_rdcss : val :=
     (* data = (l_m, m1, n1, n2, p) *)
     let l_ghost = ref #() in
     let n_new = (if !l_m = m1 then n1 else n2) in
-      Resolve (CAS l_n (InjR l_descr) (ref (InjL n_new))) p l_ghost ; #().
+      Resolve (CmpXchg l_n (InjR l_descr) (ref (InjL n_new))) p l_ghost ; #().
  *)
 Definition complete : val :=
   λ: "l_descr" "l_n",
@@ -56,7 +55,7 @@ Definition complete : val :=
     let: "p"   := Snd ("data") in
     let: "l_ghost" := ref #() in
     let: "n_new" := (if: !"l_m" = "m1" then "n2" else "n1") in
-    Resolve (CAS "l_n" (InjR "l_descr") (InjL "n_new")) "p" "l_ghost" ;; #().
+    Resolve (CmpXchg "l_n" (InjR "l_descr") (InjL "n_new")) "p" "l_ghost" ;; #().
 
 (*
   get(l_n) :=
@@ -81,10 +80,10 @@ Definition get : val :=
     let p := NewProph in
     let l_descr := ref (l_m, m1, n1, n2, p) in
     (rec: rdcss_inner()
-       let r := CAS(l_n, InjL n1, InjR l_descr) in
+       let (r, b) := CmpXchg(l_n, InjL n1, InjR l_descr) in
        match r with
          InjL n => 
-           if n = n1 then
+           if b then
              complete(l_descr, l_n) ; n1
            else
              n
@@ -101,15 +100,15 @@ Definition rdcss: val :=
     let: "l_descr" := ref ("l_m", "m1", "n1", "n2", "p") in
     (* start rdcss computation with allocated descriptor *)
     ( rec: "rdcss_inner" "_" :=
-        let: "r" := (CAS "l_n" (InjL "n1") (InjR "l_descr")) in
-        match: "r" with
+        let: "r" := CmpXchg "l_n" (InjL "n1") (InjR "l_descr") in
+        match: Fst "r" with
           InjL "n" =>
             (* non-descriptor value read, check if CAS was successful *)
-            if: "n" = "n1" then
-              (* CAS was successful, finish operation *)
+            if: Snd "r" then
+              (* CmpXchg was successful, finish operation *)
               complete "l_descr" "l_n" ;; "n1"
             else
-              (* CAS failed, hence we could linearize at the CAS *)
+              (* CmpXchg failed, hence we could linearize at the CmpXchg *)
               "n"
         | InjR "l_descr_other" =>
             (* a descriptor from a different operation was read, try to help and then restart *)
@@ -120,9 +119,9 @@ Definition rdcss: val :=
 
 (** ** Proof setup *)
 
-Definition numUR      := authR $ optionUR $ exclR ZC.
-Definition tokenUR    := exclR unitC.
-Definition one_shotUR := csumR (exclR unitC) (agreeR unitC).
+Definition numUR      := authR $ optionUR $ exclR ZO.
+Definition tokenUR    := exclR unitO.
+Definition one_shotUR := csumR (exclR unitO) (agreeR unitO).
 
 Class rdcssG Σ := RDCSSG {
                      rdcss_numG      :> inG Σ numUR;
@@ -163,10 +162,10 @@ Section rdcss.
 
   (** Definition of the invariant *)
 
-  Fixpoint val_to_some_loc (ln: loc) (vs : list (val * val)) : option loc :=
-    match vs with
-    | (InjRV (LitV (LitLoc ln')), LitV (LitLoc l)) :: _  => if bool_decide(ln = ln') then Some l else None 
-    | _                         :: vs => val_to_some_loc ln vs
+  Fixpoint val_to_some_loc (pvs : list (val * val)) : option loc :=
+    match pvs with
+    | ((_, #true)%V, LitV (LitLoc l)) :: _  => Some l
+    | _                         :: vs => val_to_some_loc vs
     | _                               => None
     end.
 
@@ -210,10 +209,12 @@ Section rdcss.
   Definition descr_inv P Q (p : proph_id) n (l_n l_descr l_ghost_winner : loc) γ_n γ_t γ_s : iProp Σ :=
     (∃ vs, proph p vs ∗
       (own γ_s (Cinl $ Excl ()) ∗
-       (l_n ↦{1/2} InjRV #l_descr ∗ ( pending_state P n (val_to_some_loc l_descr vs) l_ghost_winner γ_n
-        ∨ accepted_state (Q #n) (val_to_some_loc l_descr vs) l_ghost_winner ))
+       (l_n ↦{1/2} InjRV #l_descr ∗ ( pending_state P n (val_to_some_loc vs) l_ghost_winner γ_n
+        ∨ accepted_state (Q #n) (val_to_some_loc vs) l_ghost_winner ))
        ∨ own γ_s (Cinr $ to_agree ()) ∗ done_state (Q #n) l_descr l_ghost_winner γ_t))%I.
 
+  Local Hint Extern 0 (environments.envs_entails _ (descr_inv _ _ _ _ _ _ _ _ _ _)) => unfold descr_inv.
+
   Definition pau P Q γ l_m m1 n1 n2 :=
     (▷ P -∗ ◇ AU << ∀ (m n : Z), (gc_mapsto l_m #m) ∗ rdcss_content γ n >> @ (⊤∖↑N)∖↑gcN, ∅
                  << (gc_mapsto l_m #m) ∗ (rdcss_content γ (if (decide ((m = m1) ∧ (n = n1))) then n2 else n)),
@@ -269,7 +270,7 @@ Section rdcss.
     apply (iffLR (frac_valid' _)) in Hv. by apply Qp_not_plus_q_ge_1 in Hv.
   Qed.
 
-  (** Once a [state] protocol is [done] (as reflected by the [γ_s] token here),
+  (** Once a [descr] protocol is [done] (as reflected by the [γ_s] token here),
       we can at any later point in time extract the [Q]. *)
   Lemma state_done_extract_Q P Q p n l_n l_descr l_ghost γ_n γ_t γ_s :
     inv descrN (descr_inv P Q p n l_n l_descr l_ghost γ_n γ_t γ_s) -∗
@@ -300,7 +301,7 @@ Section rdcss.
     l_ghost ↦{1 / 2} #() -∗
     (□(own_token γ_t ={⊤}=∗ ▷ (Q #n1)) -∗ Φ #()) -∗
     own γ_n (● Excl' n) -∗
-    WP Resolve (CAS #l_n (InjRV #l_descr) (InjLV #n)) #p #l_ghost ;; #() {{ v, Φ v }}.
+    WP Resolve (CmpXchg #l_n (InjRV #l_descr) (InjLV #n)) #p #l_ghost ;; #() {{ v, Φ v }}.
   Proof.
     iIntros "#InvC #InvS Hl_ghost HQ Hn●". wp_bind (Resolve _ _ _)%E.
     iInv rdcssN as (s) "(>Hln & Hrest)".
@@ -328,8 +329,8 @@ Section rdcss.
     iDestruct "Hrest" as (q P' Q' l_ghost' γ_t' γ_s') "([>Hld >Hld'] & Hrest)".
     (* We perform the CAS. *)
     iCombine "Hln Hln'" as "Hln".
-    wp_apply (wp_resolve with "Hp"); first done. wp_cas_suc.
-    iIntros (vs' ->) "Hp'". simpl. case_bool_decide; simplify_eq.
+    wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_suc.
+    iIntros (vs' ->) "Hp'". simpl.
     (* Update to Done. *)
     iDestruct "Accepted" as "[Hl_ghost_inv [HEq Q]]".
     iMod (own_update with "Hs") as "Hs".
@@ -352,7 +353,7 @@ Section rdcss.
     inv rdcssN (rdcss_inv γ_n l_n) -∗
     inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost_inv γ_n γ_t γ_s) -∗
     (□(own_token γ_t ={⊤}=∗ ▷ (Q #n1)) -∗ Φ #()) -∗
-    WP Resolve (CAS #l_n (InjRV #l_descr) (InjLV #n)) #p #l_ghost ;; #() {{ v, Φ v }}.
+    WP Resolve (CmpXchg #l_n (InjRV #l_descr) (InjLV #n)) #p #l_ghost ;; #() {{ v, Φ v }}.
   Proof.
     iIntros (Hnl) "#InvC #InvS HQ". wp_bind (Resolve _ _ _)%E.
     iInv rdcssN as (s) "(>Hln & Hrest)".
@@ -364,8 +365,8 @@ Section rdcss.
         iDestruct "NotDone" as "(_ & >Hln' & State)".
         iDestruct (mapsto_agree with "Hln Hln'") as %[=->].
         iCombine "Hln Hln'" as "Hlln".
-        wp_apply (wp_resolve with "Hp"); first done; wp_cas_suc.
-        iIntros (vs' ->). simpl. case_bool_decide; simplify_eq.
+        wp_apply (wp_resolve with "Hp"); first done; wp_cmpxchg_suc.
+        iIntros (vs' ->). simpl.
         iDestruct "State" as "[Pending | Accepted]".
         + iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
         + iDestruct "Accepted" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs. }
@@ -374,10 +375,10 @@ Section rdcss.
     destruct s as [n' |l_descr' ].
     { (* (injL n) is the current value, hence the CAS fails *)
       (* FIXME: proof duplication *)
-      wp_apply (wp_resolve with "Hp"); first done. wp_cas_fail.
+      wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
       iIntros (vs' ->) "Hp". iModIntro.
-      iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.
-      iSplitL "Hln Hrest". { iNext. iExists _. iFrame. iFrame. }
+      iSplitL "Done Hp". { by eauto 12 with iFrame. } iModIntro.
+      iSplitL "Hln Hrest". { by eauto 12 with iFrame. }
       wp_seq. iApply "HQ".
       iApply state_done_extract_Q; done.
     }
@@ -392,10 +393,10 @@ Section rdcss.
       rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hld Hld''") as "[]".
     }
     (* The CAS fails. *)
-    wp_apply (wp_resolve with "Hp"); first done. wp_cas_fail.
+    wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
     iIntros (vs' ->) "Hp". iModIntro.
-    iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.
-    iSplitL "Hln Hrest". { iNext. iExists _. iFrame. iFrame. }
+    iSplitL "Done Hp". { by eauto 12 with iFrame. } iModIntro.
+    iSplitL "Hln Hrest". { by eauto 12 with iFrame. }
     wp_seq. iApply "HQ".
     iApply state_done_extract_Q; done.
   Qed.
@@ -452,10 +453,10 @@ Section rdcss.
         iModIntro. iSplitL "Q Hl_ghost' Hp Hvs Hs Hln'".
         { iModIntro. iNext. iExists _. iFrame "Hp". iLeft. iFrame.
           iRight. iSplitL "Hl_ghost'"; first by iExists _.
-          destruct (val_to_some_loc l_descr vs) eqn:Hvts; iFrame. }
+          destruct (val_to_some_loc vs) eqn:Hvts; iFrame. }
         (* close outer inv *)
         iModIntro. iSplitR "Hl_ghost'2 HQ Hn●".
-        { iModIntro. iExists _. iFrame. eauto. }
+        { by eauto 12 with iFrame. }
         iModIntro.
         destruct (decide (m' = m1)) as [-> | ?];
         wp_op;
@@ -491,24 +492,22 @@ Section rdcss.
 
   (** ** Proof of [rdcss] *)
   Lemma rdcss_spec γ_n v (l_m: loc) (m1 n1 n2: Z) :
-    is_rdcss γ_n v -∗ is_gc_loc l_m -∗ 
+    is_rdcss γ_n v -∗
     <<< ∀ (m n: Z), gc_mapsto l_m #m ∗ rdcss_content γ_n n >>>
         rdcss #l_m v #m1 #n1 #n2 @((⊤∖↑N)∖↑gcN)
     <<< gc_mapsto l_m #m ∗ rdcss_content γ_n (if decide (m = m1 ∧ n = n1) then n2 else n), RET #n >>>.
   Proof.
-    iIntros "Hrdcss #GC". iDestruct "Hrdcss" as (l_n) "(Heq & #InvR & #InvGC & Hdisj)".
+    iIntros "Hrdcss". iDestruct "Hrdcss" as (l_n) "(Heq & #InvR & #InvGC & Hdisj)".
     iDestruct "Heq" as %->. iDestruct "Hdisj" as %Hdisj. iIntros (Φ) "AU". 
     (* allocate fresh descriptor *)
     wp_lam. wp_pures. 
     wp_apply wp_new_proph; first done.
     iIntros (proph_values p') "Hp'".
     wp_let. wp_alloc l_descr as "Hld".
-    wp_let. 
+    wp_pures.
     (* invoke inner recursive function [rdcss_inner] *)
-    (* FIXME: would be nice to put iLöb here to avoid another
-       wp_pures tactic at the end *)
-    wp_pures. iLöb as "IH".
-    wp_bind (CAS _ _ _)%E.
+    iLöb as "IH".
+    wp_bind (CmpXchg _ _ _)%E.
     (* open outer invariant for the CAS *)
     iInv rdcssN as (s) "(>Hln & Hrest)".
     destruct s as [n|l_descr' lm' m1' n1' n2' p].
@@ -518,31 +517,34 @@ Section rdcss.
       destruct (decide (n1 = n)) as [-> | Hneq].
       + (* values match -> CAS is successful *)
         iCombine "Hln Hln'" as "Hln".
-        wp_cas_suc.
+        wp_cmpxchg_suc.
+        (* Take a "peek" at [AU] and abort immediately to get [gc_is_gc f]. *)
+        iMod "AU" as (b' n') "[[Hf CC] [Hclose _]]".
+        iDestruct (gc_is_gc with "Hf") as "#Hgc".
+        iMod ("Hclose" with "[Hf CC]") as "AU"; first by iFrame.
         (* Initialize new [descr] protocol .*)
         iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
         iMod (own_alloc (Excl ())) as (γ_t) "Token"; first done.
         iMod (own_alloc (Cinl $ Excl ())) as (γ_s) "Hs"; first done.
         iDestruct "Hln" as "[Hln Hln']".
-        set (winner := default l_descr (val_to_some_loc l_descr proph_values)).
+        set (winner := default l_descr (val_to_some_loc proph_values)).
         iMod (inv_alloc descrN _ (descr_inv AU_later _ _ _ _ _ winner _ _ _)
               with "[AU Hs Hp' Hln' Hn●]") as "#Hinv".
         {
           iNext. iExists _. iFrame "Hp'". iLeft. iFrame. iLeft.
-          iFrame. destruct (val_to_some_loc l_descr proph_values); simpl; done.
+          iFrame. destruct (val_to_some_loc proph_values); simpl; done.
         }
         iModIntro. iDestruct "Hld" as "[Hld1 [Hld2 Hld3]]". iSplitR "Hld2 Token".
         { (* close outer invariant *)
           iNext. iCombine "Hld1 Hld3" as "Hld1". iExists (Updating l_descr l_m m1 n n2 p').
           eauto 12 with iFrame. 
         }
-        wp_let. wp_match.
-        wp_op. case_bool_decide; simplify_eq.
-        wp_if. wp_apply (complete_spec with "[] [] [] [] [] [$Hld2]");[ done..|].
+        wp_pures.
+        wp_apply (complete_spec with "[] [] [] [] [] [$Hld2]");[ done..|].
         iIntros "Ht". iMod ("Ht" with "Token") as "Φ". by wp_seq.
       + (* values do not match -> CAS fails 
            we can commit here *)
-        wp_cas_fail.
+        wp_cmpxchg_fail.
         iMod "AU" as (m'' n'') "[[Hmâ—¯ Hnâ—¯] [_ Hclose]]"; simpl.
         (* synchronize B location *)
         iDestruct (sync_num_values with "Hn● Hn◯") as %->.
@@ -550,19 +552,18 @@ Section rdcss.
         {  destruct (decide _) as [[_ ?] | _]; [done | iFrame ]. }
         iModIntro. iSplitR "HΦ".
         { iModIntro. iExists (Quiescent n''). iFrame. }
-        wp_let. wp_match. wp_op. case_bool_decide; simplify_eq.
-        wp_if. iFrame.
+        wp_pures. iFrame.
     - (* l_n ↦ injR l_ndescr' *)
       (* a descriptor l_descr' is currently stored at l_n -> CAS fails
          try to help the on-going operation *)
-      wp_cas_fail. 
+      wp_cmpxchg_fail. 
       iModIntro.
       (* extract descr invariant *)
       iDestruct "Hrest" as (q P Q l_ghost γ_t γ_s) "([Hld1 [Hld2 Hld3]] & #InvS & #P_AU & #P_GC)".
       iSplitR "AU Hld2 Hld Hp'".
       (* close invariant, retain some permission to l_descr', so it can be read later *)
       { iModIntro. iExists (Updating l_descr' lm' m1' n1' n2' p). iFrame. eauto 12 with iFrame. }
-      wp_let. wp_match. 
+      wp_pures.
       wp_apply (complete_spec with "[] [] [] [] [] [$Hld2]"); [done..|].
       iIntros "_". wp_seq. wp_pures.
       iApply ("IH" with "AU Hp' Hld").
diff --git a/theories/logatom/rdcss/spec.v b/theories/logatom/rdcss/spec.v
index 58f9709a8bb9890f92f0ab8415c5f8a711aed69f..40b025b3cfac26dd320243705f29e0d00aebafea 100644
--- a/theories/logatom/rdcss/spec.v
+++ b/theories/logatom/rdcss/spec.v
@@ -1,7 +1,7 @@
 From stdpp Require Import namespaces.
 From iris.heap_lang Require Export lifting notation.
 From iris.program_logic Require Export atomic.
-From iris_examples.logatom.rdcss Require Export gc.
+From iris_examples.logatom.lib Require Export gc.
 Set Default Proof Using "Type".
 
 (** A general logically atomic interface for conditional increment. *)
@@ -27,8 +27,8 @@ Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
     {{{ True }}}
         new_rdcss #()
     {{{ lln γ, RET lln ; is_rdcss N γ lln ∗ rdcss_content γ 0 }}};
-  rdcss_spec N γ v lm (m1 n1 n2 : Z):
-    is_rdcss N γ v -∗ is_gc_loc lm -∗
+  rdcss_spec N γ v (lm : loc) (m1 n1 n2 : Z):
+    is_rdcss N γ v -∗
     <<< ∀ (m n: Z), gc_mapsto lm #m ∗ rdcss_content γ n >>>
         rdcss #lm v #m1 #n1 #n2 @((⊤∖↑N)∖↑gcN)
     <<< gc_mapsto lm #m ∗ rdcss_content γ (if decide (m = m1 ∧ n = n1) then n2 else n), RET #n >>>;