fix lock spec code depending on Σ

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 _.

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;

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 |}.

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 |}.

tests/heap_lang.v

 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.