also port rwlock and atomic_heap to the new style

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

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) :

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.

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

tests/atomic.ref

 1 goal
   
+  H : atomic_heap
   Σ : gFunctors
   heapGS0 : heapGS Σ
-  aheap : atomic_heap
+  atomic_heapGS0 : atomic_heapGS Σ
   Q : iProp Σ
   l : loc
   v : val

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. *)