diff --git a/CHANGELOG.md b/CHANGELOG.md
index 67524c9949b468e53883e5d15d4a0ad5a2661e09..499d197afa77ef2dabe8ffd5100829d2b539067b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -185,10 +185,15 @@ Coq 8.13 is no longer supported.
 * Extend `wp_apply` and `wp_smart_apply` to support immediately introducing the
   postcondition into the context via `as (x1 ... xn) "ipat1 ... ipatn"`.
 * Add comparison `≤` and `<` for locations. (by Arthur Azevedo de Amorim)
-* Make the generic `lock` specification a typeclass. Code that is generic about
-  lock implementations, or that instantiates that specification, needs
-  adjustment. See [iris_heap_lang/lib/lock.v](iris_heap_lang/lib/lock.v) for
-  documentation on how to work with this specification.
+* Make the generic `lock` interface a typeclass and make sure the lock code
+  does not depend on `Σ`. Code that is generic about lock implementations, or
+  that instantiates that specification, needs adjustment. See
+  [iris_heap_lang/lib/lock.v](iris_heap_lang/lib/lock.v) for documentation on
+  how to work with this specification.
+* Adjust the generic `atomic_heap` interface to follow the same pattern as
+  `lock`.
+* Add a generic `rwlock` interface and a spinning implementation.
+  (by Isaac van Bakel)
 
 **LaTeX changes:**
 
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index da60c7480b1a7c2d0be32e521e39e221a54516d7..5d1b848220050b2de0519937d27d630b773275b9 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -5,9 +5,9 @@ From iris.heap_lang Require Export derived_laws.
 From iris.heap_lang Require Import notation proofmode.
 From iris.prelude Require Import options.
 
-(** A general logically atomic interface for a heap.
-All parameters are implicit, since it is expected that there is only one
-[heapGS_gen] in scope that could possibly apply. For example:
+(** A general logically atomic interface for a heap. All parameters are
+implicit, since it is expected that there is only one [heapGS_gen] in scope that
+could possibly apply. For example:
   
   Context `{!heapGS_gen hlc Σ, !atomic_heap}.
 
@@ -15,52 +15,72 @@ Or, for libraries that require later credits:
 
   Context `{!heapGS Σ, !atomic_heap}.
 
+Only one instance of this class should ever be in scope. To write a library that
+is generic over the lock, just add a [`{!atomic_heap}] implicit parameter around
+the code and [`{!atomic_heapGS Σ}] around the proofs. To use a particular atomic
+heap instance, use [Local Existing Instance <atomic_heap instance>].
+
+When writing an instance of this class, please take care not to shadow the class
+projections (e.g., either use [Local Definition alloc] or avoid the name [alloc]
+altogether), and do not register an instance -- just make it a [Definition] that
+others can register later.
 *)
-Class atomic_heap `{!heapGS_gen hlc Σ} := AtomicHeap {
+Class atomic_heap := AtomicHeap {
   (* -- operations -- *)
   alloc : val;
   free : val;
   load : val;
   store : val;
   cmpxchg : val;
+  (** * Ghost state *)
+  (** The assumptions about [Σ], and the singleton [gname]s (if needed) *)
+  atomic_heapGS : gFunctors → Type;
   (* -- predicates -- *)
-  mapsto (l : loc) (dq: dfrac) (v : val) : iProp Σ;
+  mapsto `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (dq: dfrac) (v : val) : iProp Σ;
   (* -- mapsto properties -- *)
-  mapsto_timeless l q v :> Timeless (mapsto l q v);
-  mapsto_fractional l v :> Fractional (λ (q : Qp), mapsto l (DfracOwn q) v);
-  mapsto_persistent l v :> Persistent (mapsto l DfracDiscarded v);
-  mapsto_as_fractional l q v :>
-    AsFractional (mapsto l (DfracOwn q) v) (λ q, mapsto l (DfracOwn q) v) q;
-  mapsto_agree l dq1 dq2 v1 v2 : mapsto l dq1 v1 -∗ mapsto l dq2 v2 -∗ ⌜v1 = v2⌝;
-  mapsto_persist l dq v : mapsto l dq v ==∗ mapsto l DfracDiscarded v;
+  mapsto_timeless `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l q v :>
+    Timeless (mapsto (H:=H) l q v);
+  mapsto_fractional `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l v :>
+    Fractional (λ (q : Qp), mapsto (H:=H) l (DfracOwn q) v);
+  mapsto_persistent `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l v :>
+    Persistent (mapsto (H:=H) l DfracDiscarded v);
+  mapsto_as_fractional `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l q v :>
+    AsFractional (mapsto (H:=H) l (DfracOwn q) v) (λ q, mapsto (H:=H) l (DfracOwn q) v) q;
+  mapsto_agree `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l dq1 dq2 v1 v2 :
+    mapsto (H:=H) l dq1 v1 -∗ mapsto (H:=H) l dq2 v2 -∗ ⌜v1 = v2⌝;
+  mapsto_persist `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l dq v :
+    mapsto (H:=H) l dq v ==∗ mapsto (H:=H) l DfracDiscarded v;
   (* -- operation specs -- *)
-  alloc_spec (v : val) :
-    {{{ True }}} alloc v {{{ l, RET #l; mapsto l (DfracOwn 1) v }}};
-  free_spec (l : loc) (v : val) :
-    {{{ mapsto l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}};
-  load_spec (l : loc) :
-    ⊢ <<< ∀∀ (v : val) q, mapsto l q v >>> load #l @ ∅ <<< mapsto l q v, RET v >>>;
-  store_spec (l : loc) (w : val) :
-    ⊢ <<< ∀∀ v, mapsto l (DfracOwn 1) v >>> store #l w @ ∅
-      <<< mapsto l (DfracOwn 1) w, RET #() >>>;
+  alloc_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (v : val) :
+    {{{ True }}} alloc v {{{ l, RET #l; mapsto (H:=H) l (DfracOwn 1) v }}};
+  free_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (v : val) :
+    {{{ mapsto (H:=H) l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}};
+  load_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) :
+    ⊢ <<< ∀∀ (v : val) q, mapsto (H:=H) l q v >>> load #l @ ∅ <<< mapsto (H:=H) l q v, RET v >>>;
+  store_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (w : val) :
+    ⊢ <<< ∀∀ v, mapsto (H:=H) l (DfracOwn 1) v >>> store #l w @ ∅
+      <<< mapsto (H:=H) l (DfracOwn 1) w, RET #() >>>;
   (* 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.
   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) :
+  cmpxchg_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀∀ v, mapsto l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ∅
+    ⊢ <<< ∀∀ v, mapsto (H:=H) l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ∅
       <<< if decide (v = w1)
-          then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
+          then mapsto (H:=H) l (DfracOwn 1) w2 else mapsto (H:=H) l (DfracOwn 1) v,
         RET (v, #if decide (v = w1) then true else false) >>>;
 }.
-Global Hint Mode atomic_heap + + + : typeclass_instances.
+
+Existing Class atomic_heapGS.
+Global Hint Mode atomic_heapGS + + : typeclass_instances.
+Global Hint Extern 0 (atomic_heapGS _) => progress simpl : typeclass_instances.
 
 Local Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
 
-Definition faa_atomic {Σ} `{!heapGS_gen hlc Σ, !atomic_heap} : val :=
+Definition faa_atomic `{!atomic_heap} : val :=
   rec: "faa" "l" "n" :=
     let: "m" := load "l" in
     if: CAS "l" "m" ("m" + "n") then "m" else "faa" "l" "n".
@@ -76,11 +96,10 @@ Module notation.
 
   Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
   Notation FAA e1 e2 := (faa_atomic e1 e2).
-
 End notation.
 
 Section derived.
-  Context `{!heapGS_gen hlc Σ, !atomic_heap}.
+  Context `{!heapGS_gen hlc Σ, !atomic_heap, !atomic_heapGS Σ}.
 
   Import notation.
 
@@ -182,11 +201,12 @@ End proof.
 
 (* NOT an instance because users should choose explicitly to use it
      (using [Explicit Instance]). *)
-Definition primitive_atomic_heap `{!heapGS_gen hlc Σ} : atomic_heap :=
-  {| alloc_spec := primitive_alloc_spec;
-     free_spec := primitive_free_spec;
-     load_spec := primitive_load_spec;
-     store_spec := primitive_store_spec;
-     cmpxchg_spec := primitive_cmpxchg_spec;
-     mapsto_persist := primitive_laws.mapsto_persist;
-     mapsto_agree := primitive_laws.mapsto_agree |}.
+Definition primitive_atomic_heap : atomic_heap :=
+  {| atomic_heapGS _ := TCTrue;
+     alloc_spec _ _ _ _ := primitive_alloc_spec;
+     free_spec _ _ _ _ := primitive_free_spec;
+     load_spec _ _ _ _ := primitive_load_spec;
+     store_spec _ _ _ _ := primitive_store_spec;
+     cmpxchg_spec _ _ _ _ := primitive_cmpxchg_spec;
+     mapsto_persist _ _ _ _ := primitive_laws.mapsto_persist;
+     mapsto_agree _ _ _ _ := primitive_laws.mapsto_agree |}.
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index 4bfdddd20ae14732437227a46207ca3248d0c9db..b8c82febf7213bdde1d0326729a8a85ea8ba1e25 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -38,7 +38,7 @@ End increment_physical.
 (** Next: logically atomic increment on top of an arbitrary logically atomic heap *)
 
 Section increment.
-  Context `{!heapGS Σ, !atomic_heap}.
+  Context `{!atomic_heap}.
 
   Import atomic_heap.notation.
 
@@ -49,6 +49,8 @@ Section increment.
          then "oldv" (* return old value if success *)
          else "incr" "l".
 
+  Context `{!heapGS Σ, !atomic_heapGS Σ}.
+
   (** A proof of the incr specification that unfolds the definition of atomic
       accessors.  This is the style that most logically atomic proofs take. *)
   Lemma incr_spec_direct (l: loc) :
diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index 5c66f9c7c283d4d1c6647cade4a331233811f3d6..a7ba1b21384f940968dce1751eccfa4418b7ec7f 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -8,42 +8,52 @@ All parameters are implicit, since it is expected that there is only one
 [heapGS_gen] in scope that could possibly apply.
 
 Only one instance of this class should ever be in scope. To write a library that
-is generic over the lock, just add a [`{lock}] implicit parameter. To use a
-particular lock instance, use [Local Existing Instance <lock instance>].
+is generic over the lock, just add a [`{!lock}] implicit parameter around the
+code and [`{!lockG Σ}] around the proofs. To use a particular lock instance, use
+[Local Existing Instance <lock instance>].
 
 When writing an instance of this class, please take care not to shadow the class
 projections (e.g., either use [Local Definition newlock] or avoid the name
 [newlock] altogether), and do not register an instance -- just make it a
 [Definition] that others can register later. *)
-Class lock `{!heapGS_gen hlc Σ} := Lock {
+Class lock := Lock {
   (** * Operations *)
   newlock : val;
   acquire : val;
   release : val;
-  (** * Predicates *)
-  (** [name] is used to associate locked with [is_lock] *)
+  (** * Ghost state *)
+  (** The assumptions about [Σ] *)
+  lockG : gFunctors → Type;
+  (** [name] is used to associate [locked] with [is_lock] *)
   lock_name : Type;
+  (** * Predicates *)
   (** No namespace [N] parameter because we only expose program specs, which
   anyway have the full mask. *)
-  is_lock (γ: lock_name) (lock: val) (R: iProp Σ) : iProp Σ;
-  locked (γ: lock_name) : iProp Σ;
+  is_lock `{!heapGS_gen hlc Σ} {L : lockG Σ} (γ: lock_name) (lock: val) (R: iProp Σ) : iProp Σ;
+  locked `{!heapGS_gen hlc Σ} {L : lockG Σ} (γ: lock_name) : iProp Σ;
   (** * General properties of the predicates *)
-  is_lock_persistent γ lk R :> Persistent (is_lock γ lk R);
-  is_lock_iff γ lk R1 R2 :
-    is_lock γ lk R1 -∗ ▷ □ (R1 ∗-∗ R2) -∗ is_lock γ lk R2;
-  locked_timeless γ :> Timeless (locked γ);
-  locked_exclusive γ : locked γ -∗ locked γ -∗ False;
+  is_lock_persistent `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R :>
+    Persistent (is_lock (L:=L) γ lk R);
+  is_lock_iff `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R1 R2 :
+    is_lock (L:=L) γ lk R1 -∗ ▷ □ (R1 ∗-∗ R2) -∗ is_lock (L:=L) γ lk R2;
+  locked_timeless `{!heapGS_gen hlc Σ} {L : lockG Σ} γ :>
+    Timeless (locked (L:=L) γ);
+  locked_exclusive `{!heapGS_gen hlc Σ} {L : lockG Σ} γ :
+    locked (L:=L) γ -∗ locked (L:=L) γ -∗ False;
   (** * Program specs *)
-  newlock_spec (R : iProp Σ) :
-    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}};
-  acquire_spec γ lk R :
-    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}};
-  release_spec γ lk R :
-    {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}
+  newlock_spec `{!heapGS_gen hlc Σ} {L : lockG Σ} (R : iProp Σ) :
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock (L:=L) γ lk R }}};
+  acquire_spec `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R :
+    {{{ is_lock (L:=L) γ lk R }}} acquire lk {{{ RET #(); locked (L:=L) γ ∗ R }}};
+  release_spec `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R :
+    {{{ is_lock (L:=L) γ lk R ∗ locked (L:=L) γ ∗ R }}} release lk {{{ RET #(); True }}}
 }.
-Global Hint Mode lock + + + : typeclass_instances.
 
-Global Instance is_lock_contractive `{!heapGS_gen hlc Σ, !lock} γ lk :
+Existing Class lockG.
+Global Hint Mode lockG + + : typeclass_instances.
+Global Hint Extern 0 (lockG _) => progress simpl : typeclass_instances.
+
+Global Instance is_lock_contractive `{!heapGS_gen hlc Σ, !lock, !lockG Σ} γ lk :
   Contractive (is_lock γ lk).
 Proof.
   apply (uPred.contractive_internal_eq (M:=iResUR Σ)).
@@ -52,5 +62,5 @@ Proof.
     iNext; iRewrite "HPQ"; auto.
 Qed.
 
-Global Instance is_lock_proper `{!heapGS_gen hlc Σ, !lock} γ lk :
+Global Instance is_lock_proper `{!heapGS_gen hlc Σ, !lock, !lockG Σ} γ lk :
   Proper ((≡) ==> (≡)) (is_lock γ lk) := ne_proper _.
diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index e2cddb9ee597d2d1815449c9bd4d4814c0c96893..859fea3d5c193275f0e228cd08050cff813a9fb6 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -18,14 +18,14 @@ From iris.prelude Require Import options.
 
 Inductive state := Free | Locked.
 
-Class lockG Σ := LockG { lock_tokG : ghost_varG Σ state }.
+Class alockG Σ := LockG { lock_tokG : ghost_varG Σ state }.
 Local Existing Instance lock_tokG.
-Definition lockΣ : gFunctors := #[ghost_varΣ state].
-Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Definition alockΣ : gFunctors := #[ghost_varΣ state].
+Global Instance subG_alockΣ {Σ} : subG alockΣ Σ → alockG Σ.
 Proof. solve_inG. Qed.
 
 Section tada.
-  Context `{!heapGS Σ, !lockG Σ, !lock}.
+  Context `{!heapGS Σ, !alockG Σ, !lock, !lockG Σ}.
 
   Record tada_lock_name := TadaLockName {
     tada_lock_name_state : gname;
diff --git a/iris_heap_lang/lib/rw_lock.v b/iris_heap_lang/lib/rw_lock.v
index 7eb3572632e6ab251f9161cfc3779bc41497317f..d42ed7c52d72c55f8bf450f6852e69d31c324f67 100644
--- a/iris_heap_lang/lib/rw_lock.v
+++ b/iris_heap_lang/lib/rw_lock.v
@@ -9,62 +9,74 @@ All parameters are implicit, since it is expected that there is only one
 [heapGS_gen] in scope that could possibly apply.
 
 Only one instance of this class should ever be in scope. To write a library that
-is generic over the lock, just add a [`{rwlock}] implicit parameter. To use a
-particular lock instance, use [Local Existing Instance <rwlock instance>].
+is generic over the lock, just add a [`{!rwlock}] implicit parameter around the
+code and [`{!rwlockG Σ}] around the proofs. To use a particular lock instance,
+use [Local Existing Instance <rwlock instance>].
 
 When writing an instance of this class, please take care not to shadow the class
 projections (e.g., either use [Local Definition newlock] or avoid the name
- [newlock] altogether), and do not register an instance -- just make it a
+[newlock] altogether), and do not register an instance -- just make it a
 [Definition] that others can register later. *)
-Class rwlock `{!heapGS_gen hlc Σ} := RwLock {
+Class rwlock := RwLock {
   (** * Operations *)
   newlock : val;
   acquire_reader : val;
   release_reader : val;
   acquire_writer : val;
   release_writer : val;
-  (** * Predicates *)
+  (** * Ghost state *)
+  (** The assumptions about [Σ] *)
+  rwlockG : gFunctors → Type;
   (** [lock_name] is used to associate [reader_locked] and [writer_locked] with
   [is_rw_lock] *)
   lock_name : Type;
+  (** * Predicates *)
   (** No namespace [N] parameter because we only expose program specs, which
   anyway have the full mask. *)
-  is_rw_lock (γ : lock_name) (lock : val) (Φ : Qp → iProp Σ) : iProp Σ;
-  reader_locked (γ : lock_name) (q : Qp) : iProp Σ;
-  writer_locked (γ : lock_name) : iProp Σ;
+  is_rw_lock `{!heapGS_gen hlc Σ} {L : rwlockG Σ} (γ : lock_name) (lock : val) (Φ : Qp → iProp Σ) : iProp Σ;
+  reader_locked `{!heapGS_gen hlc Σ} {L : rwlockG Σ} (γ : lock_name) (q : Qp) : iProp Σ;
+  writer_locked `{!heapGS_gen hlc Σ} {L : rwlockG Σ} (γ : lock_name) : iProp Σ;
   (** * General properties of the predicates *)
-  is_rw_lock_persistent γ lk Φ :> Persistent (is_rw_lock γ lk Φ);
-  is_rw_lock_iff γ lk Φ Ψ :
-    is_rw_lock γ lk Φ -∗ ▷ □ (∀ q, Φ q ∗-∗ Ψ q) -∗ is_rw_lock γ lk Ψ;
-  reader_locked_timeless γ q :> Timeless (reader_locked γ q);
-  writer_locked_timeless γ :> Timeless (writer_locked γ);
-  writer_locked_exclusive γ : writer_locked γ -∗ writer_locked γ -∗ False;
-  writer_locked_not_reader_locked γ q : writer_locked γ -∗ reader_locked γ q -∗ False;
+  is_rw_lock_persistent `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ :>
+    Persistent (is_rw_lock (L:=L) γ lk Φ);
+  is_rw_lock_iff `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ Ψ :
+    is_rw_lock (L:=L) γ lk Φ -∗ ▷ □ (∀ q, Φ q ∗-∗ Ψ q) -∗ is_rw_lock (L:=L) γ lk Ψ;
+  reader_locked_timeless `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ q :>
+    Timeless (reader_locked (L:=L) γ q);
+  writer_locked_timeless `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ :>
+    Timeless (writer_locked (L:=L) γ);
+  writer_locked_exclusive `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ :
+    writer_locked (L:=L) γ -∗ writer_locked (L:=L) γ -∗ False;
+  writer_locked_not_reader_locked `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ q :
+    writer_locked (L:=L) γ -∗ reader_locked (L:=L) γ q -∗ False;
   (** * Program specs *)
-  newlock_spec (Φ : Qp → iProp Σ) `{!AsFractional P Φ 1} :
+  newlock_spec `{!heapGS_gen hlc Σ} {L : rwlockG Σ} (Φ : Qp → iProp Σ) `{!AsFractional P Φ 1} :
     {{{ P }}}
       newlock #()
-    {{{ lk γ, RET lk; is_rw_lock γ lk Φ }}};
-  acquire_reader_spec γ lk Φ :
-    {{{ is_rw_lock γ lk Φ }}}
+    {{{ lk γ, RET lk; is_rw_lock (L:=L) γ lk Φ }}};
+  acquire_reader_spec `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ :
+    {{{ is_rw_lock (L:=L) γ lk Φ }}}
       acquire_reader lk
-    {{{ q, RET #(); reader_locked γ q ∗ Φ q }}};
-  release_reader_spec γ lk Φ q :
-    {{{ is_rw_lock γ lk Φ ∗ reader_locked γ q ∗ Φ q }}}
+    {{{ q, RET #(); reader_locked (L:=L) γ q ∗ Φ q }}};
+  release_reader_spec `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ q :
+    {{{ is_rw_lock (L:=L) γ lk Φ ∗ reader_locked (L:=L) γ q ∗ Φ q }}}
       release_reader lk
     {{{ RET #(); True }}};
-  acquire_writer_spec γ lk Φ :
-    {{{ is_rw_lock γ lk Φ }}}
+  acquire_writer_spec `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ :
+    {{{ is_rw_lock (L:=L) γ lk Φ }}}
       acquire_writer lk
-    {{{ RET #(); writer_locked γ ∗ Φ 1%Qp }}};
-  release_writer_spec γ lk Φ :
-    {{{ is_rw_lock γ lk Φ ∗ writer_locked γ ∗ Φ 1%Qp }}}
+    {{{ RET #(); writer_locked (L:=L) γ ∗ Φ 1%Qp }}};
+  release_writer_spec `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ :
+    {{{ is_rw_lock (L:=L) γ lk Φ ∗ writer_locked (L:=L) γ ∗ Φ 1%Qp }}}
       release_writer lk
     {{{ RET #(); True }}};
 }.
-Global Hint Mode rwlock + + + : typeclass_instances.
 
-Global Instance is_rw_lock_contractive `{!heapGS_gen hlc Σ, !rwlock} γ lk n :
+Existing Class rwlockG.
+Global Hint Mode rwlockG + + : typeclass_instances.
+Global Hint Extern 0 (rwlockG _) => progress simpl : typeclass_instances.
+
+Global Instance is_rw_lock_contractive `{!heapGS_gen hlc Σ, !rwlock, !rwlockG Σ} γ lk n :
   Proper (pointwise_relation _ (dist_later n) ==> dist n) (is_rw_lock γ lk).
 Proof.
   assert (Contractive (is_rw_lock γ lk : (Qp -d> iPropO Σ) → _)) as Hcontr.
@@ -76,7 +88,7 @@ Proof.
   intros Φ1 Φ2 HΦ. apply Hcontr. dist_later_intro. apply HΦ.
 Qed.
 
-Global Instance is_rw_lock_proper `{!heapGS_gen hlc Σ, !rwlock} γ lk :
+Global Instance is_rw_lock_proper `{!heapGS_gen hlc Σ, !rwlock, !rwlockG Σ} γ lk :
   Proper (pointwise_relation _ (≡) ==> (≡)) (is_rw_lock γ lk).
 Proof.
   intros Φ1 Φ2 HΦ. apply equiv_dist=> n. apply is_rw_lock_contractive=> q.
diff --git a/iris_heap_lang/lib/rw_spin_lock.v b/iris_heap_lang/lib/rw_spin_lock.v
index adc93e6297d7095a3b6261724572d00d3664e3e2..2c56f71a4208317a781cd21ce4783ac21b8ff803 100644
--- a/iris_heap_lang/lib/rw_spin_lock.v
+++ b/iris_heap_lang/lib/rw_spin_lock.v
@@ -31,15 +31,15 @@ Local Definition acquire_writer : val :=
 Local Definition release_writer : val :=
   λ: "l", "l" <- #0.
 
-Class rwlockG Σ := RwLockG { rwlock_tokG : inG Σ (authR (gmultisetUR Qp)) }.
+Class rw_spin_lockG Σ := RwLockG { rwlock_tokG : inG Σ (authR (gmultisetUR Qp)) }.
 Local Existing Instance rwlock_tokG.
 
-Local Definition rwlockΣ : gFunctors := #[GFunctor (authR (gmultisetUR Qp)) ].
-Global Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
+Definition rw_spin_lockΣ : gFunctors := #[GFunctor (authR (gmultisetUR Qp)) ].
+Global Instance subG_rw_spin_lockΣ {Σ} : subG rw_spin_lockΣ Σ → rw_spin_lockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{!heapGS_gen hlc Σ, !rwlockG Σ}.
+  Context `{!heapGS_gen hlc Σ, !rw_spin_lockG Σ}.
   Let N := nroot .@ "rw_lock".
 
   Local Definition rw_state_inv (γ : gname) (l : loc) (Φ : Qp → iProp Σ) : iProp Σ :=
@@ -374,12 +374,13 @@ Section proof.
   Qed.
 End proof.
 
-Definition rw_spin_lock `{!heapGS_gen hlc Σ, !rwlockG Σ} : rwlock :=
-  {| rw_lock.writer_locked_exclusive := writer_locked_exclusive;
-     rw_lock.writer_locked_not_reader_locked := writer_locked_not_reader_locked;
-     rw_lock.is_rw_lock_iff := is_rw_lock_iff;
-     rw_lock.newlock_spec := newlock_spec;
-     rw_lock.acquire_reader_spec := acquire_reader_spec;
-     rw_lock.release_reader_spec := release_reader_spec;
-     rw_lock.acquire_writer_spec := acquire_writer_spec;
-     rw_lock.release_writer_spec := release_writer_spec |}.
+Definition rw_spin_lock : rwlock :=
+  {| rw_lock.rwlockG := rw_spin_lockG;
+     rw_lock.writer_locked_exclusive _ _ _ _ := writer_locked_exclusive;
+     rw_lock.writer_locked_not_reader_locked _ _ _ _ := writer_locked_not_reader_locked;
+     rw_lock.is_rw_lock_iff _ _ _ _ := is_rw_lock_iff;
+     rw_lock.newlock_spec _ _ _ _ := newlock_spec;
+     rw_lock.acquire_reader_spec _ _ _ _ := acquire_reader_spec;
+     rw_lock.release_reader_spec _ _ _ _ := release_reader_spec;
+     rw_lock.acquire_writer_spec _ _ _ _ := acquire_writer_spec;
+     rw_lock.release_writer_spec _ _ _ _ := release_writer_spec |}.
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 8686e3e03de742d8dc0fc86ffbaf1f4e323bf2fe..9055ad13866ce9c3798b0dc15969ad83a5ed2451 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -14,16 +14,16 @@ Local Definition release : val := λ: "l", "l" <- #false.
 
 (** The CMRA we need. *)
 (* Not bundling heapGS, as it may be shared with other users. *)
-Class lockG Σ := LockG { lock_tokG : inG Σ (exclR unitO) }.
+Class spin_lockG Σ := LockG { lock_tokG : inG Σ (exclR unitO) }.
 Local Existing Instance lock_tokG.
 
-Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
+Definition spin_lockΣ : gFunctors := #[GFunctor (exclR unitO)].
 
-Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Global Instance subG_spin_lockΣ {Σ} : subG spin_lockΣ Σ → spin_lockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{!heapGS_gen hlc Σ, !lockG Σ}.
+  Context `{!heapGS_gen hlc Σ, !spin_lockG Σ}.
   Let N := nroot .@ "spin_lock".
 
   Local Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
@@ -92,7 +92,12 @@ Section proof.
   Qed.
 End proof.
 
-Definition spin_lock `{!heapGS_gen hlc Σ, !lockG Σ} : lock :=
-  {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
-     lock.newlock_spec := newlock_spec;
-     lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
+(* NOT an instance because users should choose explicitly to use it
+     (using [Explicit Instance]). *)
+Definition spin_lock : lock :=
+  {| lock.lockG := spin_lockG;
+     lock.locked_exclusive _ _ _ _ := locked_exclusive;
+     lock.is_lock_iff _ _ _ _ := is_lock_iff;
+     lock.newlock_spec _ _ _ _ := newlock_spec;
+     lock.acquire_spec _ _ _ _ := acquire_spec;
+     lock.release_spec _ _ _ _ := release_spec |}.
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index 02c4e48d071cb9983206c99655b54317ebc2e52d..0f9f1f47d42ba13fd38841dd1ba53191852f2b26 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -163,7 +163,10 @@ Section proof.
   Qed.
 End proof.
 
-Definition ticket_lock `{!heapGS_gen hlc Σ, !tlockG Σ} : lock :=
-  {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
-     lock.newlock_spec := newlock_spec;
-     lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
+Definition ticket_lock : lock :=
+  {| lock.lockG := tlockG;
+     lock.locked_exclusive _ _ _ _ := locked_exclusive;
+     lock.is_lock_iff _ _ _ _ := is_lock_iff;
+     lock.newlock_spec _ _ _ _ := newlock_spec;
+     lock.acquire_spec _ _ _ _ := acquire_spec;
+     lock.release_spec _ _ _ _ := release_spec |}.
diff --git a/tests/atomic.ref b/tests/atomic.ref
index d582612c72f7c1e8672f0b75dad074e70f301635..90a359e12dfccdd617576282f4644185eed71eef 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -1,8 +1,9 @@
 1 goal
   
+  H : atomic_heap
   Σ : gFunctors
   heapGS0 : heapGS Σ
-  aheap : atomic_heap
+  atomic_heapGS0 : atomic_heapGS Σ
   Q : iProp Σ
   l : loc
   v : val
diff --git a/tests/atomic.v b/tests/atomic.v
index 173a45f01786e683b76ae5f5481fcc4131cfa5e6..32b5595bca4177690914c8c607b8ce369aac7615 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -22,7 +22,7 @@ Section general_bi_tests.
 End general_bi_tests.
 
 Section tests.
-  Context `{!heapGS Σ} {aheap: atomic_heap}.
+  Context `{!atomic_heap, !heapGS Σ, !atomic_heapGS Σ}.
   Import atomic_heap.notation.
 
   (* FIXME: removing the `val` type annotation breaks printing. *)
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 96d71b08ba31fb59e1cd40c36731cd0e72ff15a2..c5f966bb02e09ec68c1dad0510804e8aca7e01ad 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Import gen_inv_heap invariants.
 From iris.program_logic Require Export weakestpre total_weakestpre.
-From iris.heap_lang Require Import lang adequacy total_adequacy proofmode notation lib.lock.
+From iris.heap_lang Require Import lang adequacy total_adequacy proofmode notation lib.spin_lock.
 From iris.prelude Require Import options.
 
 Unset Mangle Names.
@@ -516,7 +516,7 @@ Qed.
 
 (** Just making sure the lock typeclass actually works. *)
 Section lock.
-  Context `{!heapGS Σ, !lock}.
+  Context `{!lock}.
 
   Definition lock_client : val :=
     λ: "loc" "lock",
@@ -524,6 +524,8 @@ Section lock.
       "loc" <- #42;;
       release "lock".
 
+  Context `{!heapGS Σ, !lockG Σ}.
+
   Lemma wp_lock_client loc lock γ :
     is_lock γ lock (∃ v, loc ↦ v) -∗
     WP lock_client #loc lock {{ _, True }}.
@@ -535,6 +537,28 @@ Section lock.
     { iFrame "Hislock". eauto. }
     eauto.
   Qed.
-
 End lock.
+Section spin_lock.
+  Local Existing Instance spin_lock.
 
+  Definition spin_lock_client : val :=
+    λ: "loc" "lock",
+      acquire "lock";;
+      "loc" <- #42;;
+      release "lock".
+
+  (* Making sure that using [spin_lockG] here works, not just [lockG]. *)
+  Context `{!heapGS Σ, !spin_lockG Σ}.
+
+  Lemma wp_spin_lock_client loc lock γ :
+    is_lock γ lock (∃ v, loc ↦ v) -∗
+    WP spin_lock_client #loc lock {{ _, True }}.
+  Proof.
+    iIntros "#Hislock".
+    wp_lam. wp_smart_apply (acquire_spec with "Hislock") as "[Hlocked [%v Hloc]]".
+    wp_store.
+    wp_smart_apply (release_spec with "[$Hlocked Hloc]").
+    { iFrame "Hislock". eauto. }
+    eauto.
+  Qed.
+End spin_lock.