diff --git a/_CoqProject b/_CoqProject
index 42e6e96ce7f2688c07946d50d67fb8415f7d87c5..cbad095135a6d494daaeb4ad166a9e289fe900a8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -168,8 +168,10 @@ iris_heap_lang/lib/spawn.v
 iris_heap_lang/lib/par.v
 iris_heap_lang/lib/assert.v
 iris_heap_lang/lib/lock.v
+iris_heap_lang/lib/rw_lock.v
 iris_heap_lang/lib/spin_lock.v
 iris_heap_lang/lib/ticket_lock.v
+iris_heap_lang/lib/rw_spin_lock.v
 iris_heap_lang/lib/nondet_bool.v
 iris_heap_lang/lib/lazy_coin.v
 iris_heap_lang/lib/clairvoyant_coin.v
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index d87eebacce526fa57d456abe8cd75f654ba3368b..797b59d843596ecdb8370ddaa919fd6af8f628a4 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -1,5 +1,5 @@
 From iris.bi Require Export bi.
-From iris.proofmode Require Import classes classes_make.
+From iris.proofmode Require Import classes classes_make proofmode.
 From iris.prelude Require Import options.
 
 Class Fractional {PROP : bi} (Φ : Qp → PROP) :=
@@ -196,3 +196,39 @@ Section fractional.
     by rewrite bi.intuitionistically_if_elim fractional.
   Qed.
 End fractional.
+
+Section internal_fractional.
+  Context {PROP : bi}.
+  Implicit Types Φ Ψ : Qp → PROP.
+  Implicit Types q : Qp.
+
+  Global Definition internal_fractional Φ
+    := (□ (∀ p q, Φ (p + q)%Qp ∗-∗ Φ p ∗ Φ q))%I.
+  Global Instance internal_fractional_persistent Φ :
+    Persistent (internal_fractional Φ) := _.
+
+  Global Lemma fractional_internal_fractional Φ :
+    Fractional Φ → ⊢ internal_fractional Φ.
+  Proof.
+    intros frac.
+    iIntros "!>" (q1 q2).
+    rewrite [Φ (q1 + q2)%Qp]frac //=;  auto.
+  Qed.
+
+  Global Lemma internal_fractional_iff `{!BiAffine PROP} Φ Ψ:
+    □ (∀ q, Φ q ↔ Ψ q) ⊢ internal_fractional Φ -∗ internal_fractional Ψ.
+  Proof.
+    iIntros "#Hiff #HΦdup !>" (p q).
+    iSplit.
+    - iIntros "H".
+      iDestruct ("Hiff" with "H") as "HΦ".
+      iDestruct ("HΦdup" with "HΦ") as "[H1 ?]".
+      iSplitL "H1"; iApply "Hiff"; iFrame.
+    - iIntros "[H1 H2]".
+      iDestruct ("Hiff" with "H1") as "HΦ1".
+      iDestruct ("Hiff" with "H2") as "HΦ2".
+      iApply "Hiff".
+      iApply "HΦdup".
+      iFrame.
+  Qed.
+End internal_fractional.
diff --git a/iris_heap_lang/lib/rw_lock.v b/iris_heap_lang/lib/rw_lock.v
new file mode 100644
index 0000000000000000000000000000000000000000..85bd529554ed1f7259c6b1e86401d22e98d87d38
--- /dev/null
+++ b/iris_heap_lang/lib/rw_lock.v
@@ -0,0 +1,65 @@
+From iris.base_logic.lib Require Export invariants.
+From iris.bi.lib Require Export fractional.
+From iris.heap_lang Require Import primitive_laws notation.
+From iris.prelude Require Import options.
+
+(** A general interface for a reader-writer lock.
+
+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>].
+
+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 rwlock `{!heapGS_gen hlc Σ} := RwLock {
+  (** * Operations *)
+  newlock : val;
+  acquire_reader : val;
+  release_reader : val;
+  acquire_writer : val;
+  release_writer : val;
+  (** * Predicates *)
+  (** [lock_name] is used to associate [reader_locked] and [writer_locked] with
+  [is_rw_lock] *)
+  lock_name : Type;
+  (** 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 Σ;
+  (** * 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;
+  (** * Program specs *)
+  newlock_spec (Φ : Qp → iProp Σ) `{!AsFractional P Φ 1} :
+    {{{ P }}}
+      newlock #()
+    {{{ lk γ, RET lk; is_rw_lock γ lk Φ }}};
+  acquire_reader_spec γ lk Φ :
+    {{{ is_rw_lock γ lk Φ }}}
+      acquire_reader lk
+    {{{ q, RET #(); reader_locked γ q ∗ Φ q }}};
+  release_reader_spec γ lk Φ q :
+    {{{ is_rw_lock γ lk Φ ∗ reader_locked γ q ∗ Φ q }}}
+      release_reader lk
+    {{{ RET #(); True }}};
+  acquire_writer_spec γ lk Φ :
+    {{{ is_rw_lock γ lk Φ }}}
+      acquire_writer lk
+    {{{ RET #(); writer_locked γ ∗ Φ 1%Qp }}};
+  release_writer_spec γ lk Φ :
+    {{{ is_rw_lock γ lk Φ ∗ writer_locked γ ∗ Φ 1%Qp }}}
+      release_writer lk
+    {{{ RET #(); True }}};
+}.
+Global Hint Mode rwlock + + + : typeclass_instances.
+
diff --git a/iris_heap_lang/lib/rw_spin_lock.v b/iris_heap_lang/lib/rw_spin_lock.v
new file mode 100644
index 0000000000000000000000000000000000000000..c2e60ea52953d1b0249dee98963e485688e34e9d
--- /dev/null
+++ b/iris_heap_lang/lib/rw_spin_lock.v
@@ -0,0 +1,397 @@
+From stdpp Require Import numbers.
+From iris.algebra Require Import gmultiset.
+From iris.base_logic Require Import invariants.
+From iris.bi.lib Require Export fractional.
+From iris.proofmode Require Import proofmode.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang.lib Require Export rw_lock.
+From iris.prelude Require Import options.
+
+Local Definition newlock : val := λ: <>, ref #0.
+Local Definition try_acquire_reader : val :=
+  λ: "l",
+    let: "n" := !"l" in
+    if: #0 ≤ "n"
+      then CAS "l" "n" ("n" + #1)
+      else #false.
+Local Definition acquire_reader : val :=
+  rec: "acquire" "l" :=
+    if: try_acquire_reader "l"
+      then #()
+      else "acquire" "l".
+Local Definition release_reader : val :=
+  λ: "l", FAA "l" #(-1) ;; #().
+Local Definition try_acquire_writer : val :=
+  λ: "l", CAS "l" #0 #(-1).
+Local Definition acquire_writer : val :=
+  rec: "acquire" "l" :=
+    if: try_acquire_writer "l"
+      then #()
+      else "acquire" "l".
+Local Definition release_writer : val :=
+  λ: "l", "l" <- #0.
+
+Class rwlockG Σ := 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 Σ.
+Proof. solve_inG. Qed.
+
+Section proof.
+  Context `{!heapGS_gen hlc Σ, !rwlockG Σ}.
+  Let N := nroot .@ "rw_lock".
+
+  Local Definition rw_state_inv (γ : gname) (l : loc) (Φ : Qp → iProp Σ) : iProp Σ :=
+    ∃ z : Z, l ↦ #z ∗
+      (* We need *some* ghost state that allows us to establish a contradiction in
+         the left disjunct (where the lock is write-locked) when proving [release_reader_spec],
+         so we use a fraction of the empty authoritative reader set (the rest goes to [writer_locked].)
+         Any fraction would do, but the benefit of giving over half to [writer_locked]
+         (and keeping less than half here) is that we can prove [writer_locked_exclusive].
+      *)
+      (⌜(z = -1)%Z⌝ ∗ own γ (●{# 1/4} ∅)
+      ∨ ⌜(0 ≤ z)%Z⌝ ∗ ∃ (q : Qp) (g : gmultiset Qp),
+          own γ (● g) ∗
+          ⌜size g = Z.to_nat z⌝ ∗
+          ⌜(set_fold Qp.add q g = 1)%Qp⌝ ∗
+          Φ q
+      ).
+  Local Hint Extern 0 (environments.envs_entails _ (rw_state_inv _ _ _)) =>
+    unfold rw_state_inv : core.
+
+  (* This definition is [tc_opaque] because the â–· around [internal_fractional]
+  should be preserved even when taking steps (otherwise it's more annoying to
+  re-establish.) *)
+  Local Definition is_rw_lock (γ : gname) (lk : val) (Φ : Qp → iProp Σ) : iProp Σ :=
+    tc_opaque (▷ internal_fractional Φ ∗
+      ∃ l : loc, ⌜lk = #l⌝ ∗ inv N (rw_state_inv γ l Φ))%I.
+  Global Instance is_rw_lock_persistent γ lk Φ : Persistent (is_rw_lock γ lk Φ).
+  Proof. unfold is_rw_lock, tc_opaque. apply _. Qed.
+  Local Hint Extern 0 (environments.envs_entails _ (is_rw_lock _ _ _)) =>
+    unfold is_rw_lock : core.
+
+  Local Definition reader_locked (γ : gname) (q : Qp) : iProp Σ := own γ (◯ {[+ q +]}).
+
+  Local Definition writer_locked (γ : gname) : iProp Σ := own γ (● {# 3/4} ∅).
+  Local Lemma writer_locked_exclusive γ : writer_locked γ -∗ writer_locked γ -∗ False.
+  Proof.
+    iIntros "H1 H2".
+    iCombine "H1 H2" gives "%Hvalid".
+    rewrite
+      auth_auth_dfrac_op_valid
+      dfrac_op_own
+      dfrac_valid_own in Hvalid.
+    destruct Hvalid as [Htoomuch _].
+    contradict Htoomuch.
+    auto.
+  Qed.
+
+  Lemma is_rw_lock_iff γ lk Φ Ψ :
+    is_rw_lock γ lk Φ -∗ ▷ □ (∀ q, Φ q ↔ Ψ q) -∗ is_rw_lock γ lk Ψ.
+  Proof.
+    iIntros "[#HΦdup [%l [-> #Hlockinv]]] #Hiff".
+    unfold is_rw_lock.
+    iSplitR.
+    { iApply (internal_fractional_iff with "Hiff HΦdup").  }
+    iExists l; iSplitR; first done.
+    iApply (inv_iff with "[Hlockinv Hiff //]"); iIntros "!> !>".
+    iDestruct "Hiff" as "#Hiff".
+    iClear "HΦdup Hlockinv".
+    iSplit.
+    - iIntros "[%z [? Hstate]]". iExists z. iFrame.
+      iDestruct "Hstate" as "[?|[? [% [% (? & ? & ? & ?)]]]]".
+      + iFrame.
+      + iRight.
+        iFrame.
+        iExists _, _.
+        iFrame.
+        by iApply "Hiff".
+    - iIntros "[%z [? Hstate]]". iExists z. iFrame.
+      iDestruct "Hstate" as "[?|[? [% [% (? & ? & ? & ?)]]]]".
+      + iFrame.
+      + iRight.
+        iFrame.
+        iExists _, _.
+        iFrame.
+        by iApply "Hiff".
+  Qed.
+
+  (* Some helper lemmas for "auth of a multiset" *)
+  Local Lemma auth_valid_gmultiset_singleton `{Countable A} dq (v : A) (g : gmultiset A) :
+    ✓ (● { dq } g ⋅ ◯ ({[+ v +]})) → v ∈ g.
+  Proof.
+    rewrite
+      auth_both_dfrac_valid_discrete
+      gmultiset_included
+      gmultiset_singleton_subseteq_l.
+    intros (_ & ? & _); assumption.
+  Qed.
+  Local Lemma own_auth_gmultiset_singleton_2 γ dq v g :
+    own γ (● { dq } g) ∗ own γ (◯ ({[+ v +]})) ⊢ ⌜v ∈ g⌝.
+  Proof.
+    iIntros "[Hauth Hfrag]".
+    iCombine "Hauth Hfrag" gives "%Hvalid".
+    iPureIntro.
+    apply (auth_valid_gmultiset_singleton _ _ _ Hvalid).
+  Qed.
+
+  Local Lemma newlock_spec (Φ : Qp → iProp Σ) `{!AsFractional P Φ 1}:
+    {{{ P }}}
+      newlock #()
+    {{{ lk γ, RET lk; is_rw_lock γ lk Φ }}}.
+  Proof.
+    iIntros (φ) "HΦ Hφ".
+    wp_lam.
+    iMod (own_alloc (● ∅)) as (γ) "Hγ".
+    { apply auth_auth_valid; done.  }
+    wp_alloc l as "Hl".
+    iMod (inv_alloc N _ (rw_state_inv γ l Φ) with "[-Hφ]") as "#?".
+    { rewrite [P]as_fractional.
+      eauto 10 with iFrame.
+    }
+    iApply "Hφ".
+    iSplitR.
+    { iApply fractional_internal_fractional.
+      apply (as_fractional_fractional (P:=P)).
+    }
+    eauto 10.
+  Qed.
+
+  Local Lemma try_acquire_reader_spec γ lk Φ:
+    {{{ is_rw_lock γ lk Φ }}}
+      try_acquire_reader lk
+    {{{ b, RET #b; if b is true then ∃ q, reader_locked γ q ∗ Φ q else True  }}}.
+  Proof.
+    iIntros (φ) "[#HΦdup [%l [-> #Hlockinv]]] Hφ".
+    wp_lam.
+    wp_bind (!_)%E.
+    iInv "Hlockinv" as (z) "[> Hl Hz]".
+    wp_load.
+    iSplitL "Hl Hz"; first eauto with iFrame.
+    iModIntro.
+    wp_pures.
+    destruct (Z.le_dec 0%Z z) as [Hle|?]; last first.
+    { rewrite bool_decide_false //.
+      wp_pures.
+      iApply "Hφ".
+      done.
+    }
+    rewrite bool_decide_true //.
+    wp_pures.
+    wp_bind (CmpXchg _ _ _).
+    iInv "Hlockinv" as (z') "[> Hl Hz]".
+    wp_cmpxchg as Heq|?; last first.
+    { iSplitR "Hφ".
+      { eauto with iFrame.  }
+      iModIntro.
+      wp_pures.
+      by iApply "Hφ".
+    }
+    injection Heq as ->.
+    iDestruct "Hz" as "[[-> _]|[Hz_ge_0 [%q [%g Hg]]]]"; first contradiction.
+    iDestruct "Hg" as "(Hauth & %Hsize & %Hfold & HΦ)".
+    rewrite -[q in Φ q]Qp.div_2.
+    iDestruct ("HΦdup" $! (q / 2)%Qp (q / 2)%Qp with "HΦ") as "[HΦ HΦgive]".
+    iMod (own_update _ _ (●(g ⊎ {[+ (q / 2)%Qp+]}) ⋅ ◯({[+ (q / 2)%Qp +]})) with "Hauth") as "[Hauth Hview]".
+    { apply auth_update_alloc.
+      rewrite -{2}[({[+ (q / 2)%Qp+]})]gmultiset_disj_union_left_id.
+      apply gmultiset_local_update_alloc.
+    }
+    iSplitR "HΦgive Hview Hφ".
+    { iExists (z + 1)%Z.
+      iModIntro.
+      iModIntro.
+      iFrame.
+      iRight.
+      iSplitL "Hz_ge_0"; first eauto with lia.
+      iExists _, _.
+      iFrame.
+      iSplit.
+      { iPureIntro.
+        rewrite gmultiset_size_disj_union gmultiset_size_singleton.
+        lia.
+      }
+      iPureIntro.
+      rewrite
+        gmultiset_set_fold_disj_union
+        gmultiset_set_fold_singleton
+        -gmultiset_set_fold_comm_acc.
+        { rewrite Qp.div_2 //. }
+        intros. rewrite 2!Qp.add_assoc [(_ + q/2)%Qp]Qp.add_comm //.
+    }
+    iModIntro.
+    wp_pures.
+    iApply "Hφ".
+    eauto with iFrame.
+  Qed.
+
+  Local Lemma acquire_reader_spec γ lk Φ:
+    {{{ is_rw_lock γ lk Φ }}}
+      acquire_reader lk
+    {{{ q, RET #(); reader_locked γ q ∗ Φ q }}}.
+  Proof.
+    iIntros (φ) "#Hislock Hφ".
+    iLöb as "IH".
+    wp_rec.
+    wp_apply (try_acquire_reader_spec with "Hislock"); iIntros ([|]).
+    - iIntros "[% ?]".
+      wp_if_true.
+      iApply "Hφ".
+      eauto with iFrame.
+    - iIntros.
+      wp_if_false.
+      iApply "IH".
+      eauto.
+  Qed.
+
+  Local Lemma release_reader_spec γ lk Φ q:
+    {{{ is_rw_lock γ lk Φ ∗ reader_locked γ q ∗ Φ q }}}
+      release_reader lk
+    {{{ RET #(); True }}}.
+  Proof.
+    iIntros (φ) "([#HΦdup [%l [-> Hlockinv]]] & Hlocked & HΦ) Hφ".
+    wp_lam.
+    wp_bind (FAA _ _).
+    iInv "Hlockinv" as (z) "[> Hl Hz]".
+    wp_faa.
+    unfold reader_locked.
+    iDestruct "Hz" as "[[_ Hempty]|[%Hz_ge_0 [%q' [%g (Hg & %Hsize & %Hsum & HΦq')]]]]".
+    { iExFalso.
+      iDestruct (own_auth_gmultiset_singleton_2 with "[$]") as "%".
+      multiset_solver.
+    }
+    iAssert (⌜(0 < z)%Z ∧ q ∈ g⌝)%I as "%".
+    { iDestruct (own_auth_gmultiset_singleton_2 with "[$]") as "%".
+      iPureIntro.
+      split; last assumption.
+      apply Z2Nat.neq_0_pos.
+      rewrite -Hsize gmultiset_size_empty_iff.
+      multiset_solver.
+    }
+    iCombine "Hg Hlocked" as "Hown".
+    iMod (own_update _ _ (●(g ∖ {[+ q +]})) with "Hown") as "Hown".
+    { apply auth_update_dealloc.
+      replace ε with ({[+ q +]} ∖ {[+ q +]} : gmultiset Qp); last first.
+      { rewrite gmultiset_difference_diag //.  }
+      apply gmultiset_local_update_dealloc.
+      multiset_solver.
+    }
+    iModIntro.
+    iSplitR "Hφ".
+    { iExists (z + -1)%Z.
+      iFrame.
+      iRight.
+      iSplit.
+      { eauto with lia.  }
+      iExists _, _.
+      iDestruct ("HΦdup" $! q q' with  "[HΦ HΦq']") as "HΦ"; first iFrame.
+      iModIntro.
+      iFrame.
+      iSplit.
+      { iPureIntro.
+        rewrite gmultiset_size_difference; last multiset_solver.
+        rewrite gmultiset_size_singleton.
+        lia.
+      }
+      iPureIntro.
+      rewrite -Hsum gmultiset_set_fold_comm_acc; last first.
+       { intros. rewrite 2!Qp.add_assoc [(_ + q)%Qp]Qp.add_comm //. }
+      rewrite
+        -gmultiset_set_fold_singleton
+        -gmultiset_set_fold_disj_union
+        gmultiset_disj_union_comm
+        -gmultiset_disj_union_difference //.
+      multiset_solver.
+    }
+    wp_pures.
+    by iApply "Hφ".
+  Qed.
+
+  Local Lemma try_acquire_writer_spec γ lk Φ:
+    {{{ is_rw_lock γ lk Φ }}}
+      try_acquire_writer lk
+    {{{ b, RET #b; if b is true then writer_locked γ ∗ Φ 1%Qp else True }}}.
+  Proof.
+    iIntros (φ) "[#HΦdup [%l [-> #Hlockinv]]] Hφ".
+    wp_lam.
+    wp_bind (CmpXchg _ _ _).
+    iInv ("Hlockinv") as (z) "[> Hl Hz]".
+    wp_cmpxchg as Heq|?; last first.
+    { iModIntro.
+      iSplitL "Hl Hz".
+      { eauto with iFrame.  }
+      wp_pures.
+      by iApply "Hφ".
+    }
+    injection Heq as ->.
+    iDestruct "Hz" as "[[%H0_eq_1 ?]|[_ [%q [%g (Hg & %Hsize & %Hfold & HΦ)]]]]".
+    { iExFalso.  by contradict H0_eq_1.  }
+    apply gmultiset_size_empty_inv in Hsize. subst g.
+    rewrite gmultiset_set_fold_empty in Hfold. subst q.
+    rewrite -[in (●{# 1} _)]Qp.quarter_three_quarter.
+    iDestruct "Hg" as "[Hg Hg_give]".
+    iModIntro.
+    iSplitL "Hl Hg".
+    { eauto 10 with iFrame.  }
+    wp_pures.
+    iApply "Hφ".
+    by iFrame.
+  Qed.
+
+  Local Lemma acquire_writer_spec γ lk Φ:
+    {{{ is_rw_lock γ lk Φ }}}
+      acquire_writer lk
+    {{{ RET #(); writer_locked γ ∗ Φ 1%Qp }}}.
+  Proof.
+    iIntros (φ) "#Hislock Hφ".
+    iLöb as "IH".
+    wp_rec.
+    wp_apply (try_acquire_writer_spec with "Hislock"); iIntros ([|]).
+    - iIntros.
+      wp_if_true.
+      iApply "Hφ".
+      eauto with iFrame.
+    - iIntros.
+      wp_if_false.
+      iApply "IH".
+      eauto.
+  Qed.
+
+  Local Lemma release_writer_spec γ lk Φ:
+    {{{ is_rw_lock γ lk Φ ∗ writer_locked γ ∗ Φ 1%Qp }}}
+      release_writer lk
+    {{{ RET #(); True }}}.
+  Proof.
+    iIntros (φ) "([#HΦdup [%l [-> #Hlockinv]]] & Hlocked & HΦ) Hφ".
+    wp_lam.
+    iInv ("Hlockinv") as (z) "[> Hl Hz]".
+    wp_store.
+    iDestruct "Hz" as "[[? Hg]|[_ [% [% [Hg_owned _]]]]]"; last first.
+    { iExFalso.
+      iCombine "Hg_owned Hlocked" gives "%Hvalid".
+      rewrite
+        auth_auth_dfrac_op_valid
+        dfrac_op_own
+        dfrac_valid_own in Hvalid.
+      destruct Hvalid as [Htoomuch _].
+      contradict Htoomuch.
+      auto.
+    }
+    iCombine "Hg Hlocked" as "Hown".
+    rewrite Qp.quarter_three_quarter.
+    iSplitR "Hφ"; first eauto 15 with iFrame.
+    by iApply "Hφ".
+  Qed.
+End proof.
+
+Program Definition rw_spin_lock `{!heapGS_gen hlc Σ, !rwlockG Σ} : rwlock :=
+  {| rw_lock.writer_locked_exclusive := writer_locked_exclusive;
+     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 |}.