Tweak masks of atomic triples.

heap_lang/lib/incrementer.v

@@ -10,14 +10,13 @@ Definition incr : val :=
 Global Opaque incr.
 
 Section incr.
-  Context `{!heapG Σ} (N : namespace).
+  Context `{!heapG Σ}.
 
   (* TODO: Can we have a more WP-style definition and avoid the equality? *)
   Lemma incr_atomic_spec (l : loc) :
-    heapN ⊥ N →
     heap_ctx ⊢ ⟨⟨ x : Z, l ↦ #x ⟩⟩ incr #l @ ⊤,heapN ⟨⟨ v, v = #x ∧ l ↦ #(x + 1) ⟩⟩.
   Proof.
-    iIntros (HN) "#? !#"; iIntros (P Q) "#Hvs HP".
+    iIntros "#? !#"; iIntros (P Q) "#Hvs HP".
     iLöb as "IH". wp_rec.
     wp_bind (! _)%E.
     iMod ("Hvs" with "HP") as (x) "[Hl [Hclose _]]".

program_logic/atomic.v

@@ -8,7 +8,7 @@ Definition atomic_shift `{invG Σ} {A B}
     (P : iProp Σ)
     (Φ : B → iProp Σ) : iProp Σ :=
   (□ (P ={Eo,Ei}=★ ∃ x : A,
-        α x ★ ((α x ={Ei,Eo}=★ P) ∧ (∀ v, β x v ={Ei,Eo}=★ Φ v))))%I.
+        α x ★ ((α x ={Ei,Eo}=★ P) ∧ ∀ v, β x v ={Ei,Eo}=★ Φ v)))%I.
 
 Definition atomic_triple `{irisG Λ Σ} {A}
     (Eo Ei : coPset) (* inside/outside masks *)
@@ -16,24 +16,24 @@ Definition atomic_triple `{irisG Λ Σ} {A}
     (e : expr Λ)
     (β : A → val Λ → iProp Σ) : iProp Σ := (* atomic post-condition *)
   (□ ∀ P Φ,
-    atomic_shift Ei Eo α β P Φ -★
+    atomic_shift Eo Ei α β P Φ -★
     P -★ WP e {{ Φ }})%I.
 
 Notation "⟨⟨ x , α ⟩ ⟩ e @ Eo , Ei ⟨⟨ v , β ⟩ ⟩" :=
-  (atomic_triple Ei Eo (λ x, α) e%E (λ x v, β))
+  (atomic_triple Eo Ei (λ x, α) e%E (λ x v, β))
   (at level 20, x at level 0, α, e, β at level 200,
    format "⟨⟨  x ,  α  ⟩ ⟩  e  @  Eo , Ei  ⟨⟨  v ,  β  ⟩ ⟩") : uPred_scope.
 Notation "⟨⟨ x : A , α ⟩ ⟩ e @ Eo , Ei ⟨⟨ v , β ⟩ ⟩" :=
-  (atomic_triple Ei Eo (λ x : A, α) e%E (λ x v, β))
+  (atomic_triple Eo Ei (λ x : A, α) e%E (λ x v, β))
   (at level 20, x at level 0, α, e, β at level 200,
    format "⟨⟨  x : A ,  α  ⟩ ⟩  e  @  Eo , Ei  ⟨⟨  v ,  β  ⟩ ⟩") : uPred_scope.
 
 Notation "⟨⟨ x , α ⟩ ⟩ e @ Eo , Ei ⟨⟨ v , β ⟩ ⟩" :=
-  (True ⊢ atomic_triple Ei Eo (λ x, α) e%E (λ x v, β))
+  (True ⊢ atomic_triple Eo Ei (λ x, α) e%E (λ x v, β))
   (at level 20, x at level 0, α, e, β at level 200,
    format "⟨⟨  x ,  α  ⟩ ⟩  e  @  Eo , Ei  ⟨⟨  v ,  β  ⟩ ⟩") : C_scope.
 Notation "⟨⟨ x : A , α ⟩ ⟩ e @ Eo , Ei ⟨⟨ v , β ⟩ ⟩" :=
-  (True ⊢ atomic_triple Ei Eo (λ x : A, α) e%E (λ x v, β))
+  (True ⊢ atomic_triple Eo Ei (λ x : A, α) e%E (λ x v, β))
   (at level 20, x at level 0, α, e, β at level 200,
    format "⟨⟨  x : A ,  α  ⟩ ⟩  e  @  Eo , Ei  ⟨⟨  v ,  β  ⟩ ⟩") : C_scope.
 

tests/incrementer_client.v

@@ -8,13 +8,15 @@ Definition incr_2 : val := λ: "x",
   !"l".
 
 Section incr_2.
-  Context `{!heapG Σ, !spawnG Σ} (N : namespace).
+  Context `{!heapG Σ, !spawnG Σ}.
+
+  Let N := nroot .@ "test".
 
   (* prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *)
   Lemma incr_2_safe (x : Z) :
-    heapN ⊥ N → heap_ctx ⊢ WP incr_2 #x {{ _, True }}.
+    heap_ctx ⊢ WP incr_2 #x {{ _, True }}.
   Proof.
-    iIntros (?) "#Hh". wp_let. wp_alloc l as "Hl".
+    iIntros "#Hh". wp_let. wp_alloc l as "Hl".
     iMod (inv_alloc N _ (∃ y : Z, l ↦ # y)%I with "[Hl]") as "#?"; first eauto.
     wp_let. wp_apply (wp_par (λ _, True%I) (λ _, True%I) with "[$Hh]").
     (* prove worker triple *)
@@ -30,8 +32,8 @@ Section incr_2.
         iIntros (v) "[% Hl]"; subst.
         iMod "Hclose'". iMod ("Hclose" with "[Hl]"); eauto. }
     repeat iSplitL.
-    - by iApply (incr_atomic_spec N with "Hh * Hvs").
-    - by iApply (incr_atomic_spec N with "Hh * Hvs").
+    - iApply (incr_atomic_spec with "Hh * Hvs"); auto with ndisj.
+    - iApply (incr_atomic_spec with "Hh * Hvs"); auto with ndisj.
     - iIntros (v1 v2) "_ !>". wp_seq.
       iInv N as (y) ">Hl" "Hclose".
       wp_load. iApply "Hclose"; eauto.