diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index c71a4b675a05c02c98a71e38f9d0c9318bb31af1..579e9239c1e4472ac268e0991453c928708fd1a1 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -5,8 +5,6 @@ From iris.proofmode Require Import invariants ghost_ownership coq_tactics.
 From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
-Definition counterN : namespace := nroot .@ "counter".
-
 Definition newcounter : val := λ: <>, ref #0.
 Definition inc : val :=
   rec: "inc" "l" :=
@@ -28,17 +26,19 @@ Local Notation iProp := (iPropG heap_lang Σ).
 Definition counter_inv (l : loc) (n : mnat) : iProp := (l ↦ #n)%I.
 
 Definition counter (l : loc) (n : nat) : iProp :=
-  (∃ γ, heap_ctx ∧ auth_ctx γ counterN (counter_inv l) ∧ auth_own γ (n:mnat))%I.
+  (∃ N γ, heapN ⊥ N ∧ heap_ctx ∧
+          auth_ctx γ N (counter_inv l) ∧ auth_own γ (n:mnat))%I.
 
 (** The main proofs. *)
 Global Instance counter_persistent l n : PersistentP (counter l n).
 Proof. apply _. Qed.
 
-Lemma newcounter_spec (R : iProp) Φ :
+Lemma newcounter_spec N (R : iProp) Φ :
+  heapN ⊥ N →
   heap_ctx ★ (∀ l, counter l 0 -★ Φ #l) ⊢ WP newcounter #() {{ Φ }}.
 Proof.
-  iIntros "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
-  iPvs (auth_alloc (counter_inv l) counterN _ (O:mnat) with "[Hl]")
+  iIntros (?) "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
+  iPvs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
     as (γ) "[#? Hγ]"; try by auto.
   iPvsIntro. iApply "HΦ". rewrite /counter; eauto 10.
 Qed.
@@ -47,13 +47,13 @@ Lemma inc_spec l j (Φ : val → iProp) :
   counter l j ★ (counter l (S j) -★ Φ #()) ⊢ WP inc #l {{ Φ }}.
 Proof.
   iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
-  iDestruct "Hl" as (γ) "(#Hh & #Hγ & Hγf)".
+  iDestruct "Hl" as (N γ) "(% & #? & #Hγ & Hγf)".
   wp_focus (! _)%E.
-  iApply (auth_fsa (counter_inv l) (wp_fsa _) _ counterN); auto with fsaV.
+  iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
   iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /="; rewrite {2}/counter_inv.
   wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
   wp_let; wp_op. wp_focus (CAS _ _ _).
-  iApply (auth_fsa (counter_inv l) (wp_fsa _) _ counterN); auto with fsaV.
+  iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
   iIntros "{$Hγ $Hγf}"; iIntros (j'') "[% Hl] /="; rewrite {2}/counter_inv.
   destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
   - wp_cas_suc; first (by do 3 f_equal); iPvsIntro.
@@ -62,7 +62,7 @@ Proof.
     rewrite {2}/counter_inv !mnat_op_max (Nat.max_l (S _)); last abstract lia.
     rewrite Nat2Z.inj_succ -Z.add_1_l.
     iIntros "{$Hl} Hγf". wp_if.
-    iPvsIntro; iApply "HΦ"; iExists γ; repeat iSplit; eauto.
+    iPvsIntro; iApply "HΦ"; iExists N, γ; repeat iSplit; eauto.
     iApply (auth_own_mono with "Hγf"). apply mnat_included. abstract lia.
   - wp_cas_fail; first (rewrite !mnat_op_max; by intros [= ?%Nat2Z.inj]).
     iPvsIntro. iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
@@ -73,9 +73,9 @@ Lemma read_spec l j (Φ : val → iProp) :
   counter l j ★ (∀ i, ■ (j ≤ i)%nat → counter l i -★ Φ #i)
   ⊢ WP read #l {{ Φ }}.
 Proof.
-  iIntros "[Hc HΦ]". iDestruct "Hc" as (γ) "(#Hh & #Hγ & Hγf)".
+  iIntros "[Hc HΦ]". iDestruct "Hc" as (N γ) "(% & #? & #Hγ & Hγf)".
   rewrite /read. wp_let.
-  iApply (auth_fsa (counter_inv l) (wp_fsa _) _ counterN); auto with fsaV.
+  iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
   iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /=".
   wp_load; iPvsIntro; iExists (j `max` j'); iSplit.
   { iPureIntro; apply mnat_local_update; abstract lia. }
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index a9b4f3a18779dbcef00bcf26f5d354516ae5ac95..777abe5676d7479e2358918d5e0c638cdfe4afba 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -3,8 +3,6 @@ From iris.proofmode Require Import invariants ghost_ownership.
 From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
-Definition lockN : namespace := nroot .@ "lock".
-
 Definition newlock : val := λ: <>, ref #false.
 Definition acquire : val :=
   rec: "acquire" "l" :=
@@ -27,10 +25,11 @@ Definition lock_inv (γ : gname) (l : loc) (R : iProp) : iProp :=
   (∃ b : bool, l ↦ #b ★ if b then True else own γ (Excl ()) ★ R)%I.
 
 Definition is_lock (l : loc) (R : iProp) : iProp :=
-  (∃ γ, heap_ctx ∧ inv lockN (lock_inv γ l R))%I.
+  (∃ N γ, heapN ⊥ N ∧ heap_ctx ∧ inv N (lock_inv γ l R))%I.
 
 Definition locked (l : loc) (R : iProp) : iProp :=
-  (∃ γ, heap_ctx ∧ inv lockN (lock_inv γ l R) ∧ own γ (Excl ()))%I.
+  (∃ N γ, heapN ⊥ N ∧ heap_ctx ∧
+          inv N (lock_inv γ l R) ∧ own γ (Excl ()))%I.
 
 Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
 Proof. solve_proper. Qed.
@@ -44,38 +43,39 @@ Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
 Proof. apply _. Qed.
 
 Lemma locked_is_lock l R : locked l R ⊢ is_lock l R.
-Proof. rewrite /is_lock. iDestruct 1 as (γ) "(?&?&_)"; eauto. Qed.
+Proof. rewrite /is_lock. iDestruct 1 as (N γ) "(?&?&?&_)"; eauto. Qed.
 
-Lemma newlock_spec (R : iProp) Φ :
+Lemma newlock_spec N (R : iProp) Φ :
+  heapN ⊥ N →
   heap_ctx ★ R ★ (∀ l, is_lock l R -★ Φ #l) ⊢ WP newlock #() {{ Φ }}.
 Proof.
-  iIntros "(#Hh & HR & HΦ)". rewrite /newlock.
+  iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
   wp_seq. wp_alloc l as "Hl".
   iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
-  iPvs (inv_alloc lockN _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done.
+  iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done.
   { iIntros ">". iExists false. by iFrame. }
-  iPvsIntro. iApply "HΦ". iExists γ; eauto.
+  iPvsIntro. iApply "HΦ". iExists N, γ; eauto.
 Qed.
 
 Lemma acquire_spec l R (Φ : val → iProp) :
   is_lock l R ★ (locked l R -★ R -★ Φ #()) ⊢ WP acquire #l {{ Φ }}.
 Proof.
-  iIntros "[Hl HΦ]". iDestruct "Hl" as (γ) "[#Hh #?]".
+  iIntros "[Hl HΦ]". iDestruct "Hl" as (N γ) "(%&#?&#?)".
   iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
-  iInv lockN as ([]) "[Hl HR]".
+  iInv N as ([]) "[Hl HR]".
   - wp_cas_fail. iPvsIntro; iSplitL "Hl".
     + iNext. iExists true; eauto.
     + wp_if. by iApply "IH".
   - wp_cas_suc. iPvsIntro. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
     + iNext. iExists true; eauto.
-    + wp_if. iApply ("HΦ" with "[-HR] HR"). iExists γ; eauto.
+    + wp_if. iApply ("HΦ" with "[-HR] HR"). iExists N, γ; eauto.
 Qed.
 
 Lemma release_spec R l (Φ : val → iProp) :
   locked l R ★ R ★ Φ #() ⊢ WP release #l {{ Φ }}.
 Proof.
-  iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (γ) "(#Hh & #? & Hγ)".
-  rewrite /release. wp_let. iInv lockN as (b) "[Hl _]".
+  iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (N γ) "(% & #? & #? & Hγ)".
+  rewrite /release. wp_let. iInv N as (b) "[Hl _]".
   wp_store. iPvsIntro. iFrame "HΦ". iNext. iExists false. by iFrame.
 Qed.
 End proof.
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 7efd44ee5662fd2c8184db127021af93554d9d79..1d9cca643ee1a94959fa85bfcb199cfad0ffd5d4 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -2,6 +2,8 @@ From iris.heap_lang Require Export spawn.
 From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
+Definition parN : namespace := nroot .@ "par".
+
 Definition par : val :=
   λ: "fs",
     let: "handle" := spawn (Fst "fs") in
@@ -23,7 +25,7 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
 Proof.
   iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
   rewrite /par. wp_value. iPvsIntro. wp_let. wp_proj.
-  wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh".
+  wp_apply (spawn_spec parN); try wp_done; try solve_ndisj; iFrame "Hf1 Hh".
   iIntros (l) "Hl". wp_let. wp_proj. wp_focus (f2 _).
   iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let.
   wp_apply join_spec; iFrame "Hl". iIntros (w) "H1".
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 6e34021d0bd94215381824886ad56ba89388db3b..4c2617a7f09960df3b8926fb3318df376b1d8b6e 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -3,8 +3,6 @@ From iris.proofmode Require Import invariants ghost_ownership.
 From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
-Definition spawnN : namespace := nroot .@ "spawn".
-
 Definition spawn : val :=
   λ: "f",
     let: "c" := ref NONE in
@@ -30,7 +28,7 @@ Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-Context `{!heapG Σ, !spawnG Σ}.
+Context `{!heapG Σ, !spawnG Σ} (N : namespace).
 Local Notation iProp := (iPropG heap_lang Σ).
 
 Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp :=
@@ -38,7 +36,8 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp :=
                    ∃ v, lv = SOMEV v ★ (Ψ v ∨ own γ (Excl ()))))%I.
 
 Definition join_handle (l : loc) (Ψ : val → iProp) : iProp :=
-  (∃ γ, heap_ctx ★ own γ (Excl ()) ★ inv spawnN (spawn_inv γ l Ψ))%I.
+  (heapN ⊥ N ★ ∃ γ, heap_ctx ★ own γ (Excl ()) ★
+                    inv N (spawn_inv γ l Ψ))%I.
 
 Typeclasses Opaque join_handle.
 
@@ -52,18 +51,19 @@ Proof. solve_proper. Qed.
 (** The main proofs. *)
 Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
   to_val e = Some f →
+  heapN ⊥ N →
   heap_ctx ★ WP f #() {{ Ψ }} ★ (∀ l, join_handle l Ψ -★ Φ #l)
   ⊢ WP spawn e {{ Φ }}.
 Proof.
-  iIntros (<-%of_to_val) "(#Hh & Hf & HΦ)". rewrite /spawn.
+  iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn.
   wp_let. wp_alloc l as "Hl". wp_let.
   iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
-  iPvs (inv_alloc spawnN _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
+  iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
   { iNext. iExists NONEV. iFrame; eauto. }
   wp_apply wp_fork. iSplitR "Hf".
   - iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto.
   - wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
-    iInv spawnN as (v') "[Hl _]".
+    iInv N as (v') "[Hl _]".
     wp_store. iPvsIntro. iSplit; [iNext|done].
     iExists (SOMEV v). iFrame. eauto.
 Qed.
@@ -71,8 +71,8 @@ Qed.
 Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
   join_handle l Ψ ★ (∀ v, Ψ v -★ Φ v) ⊢ WP join #l {{ Φ }}.
 Proof.
-  rewrite /join_handle; iIntros "[H Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
-  iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv spawnN as (v) "[Hl Hinv]".
+  rewrite /join_handle; iIntros "[[% H] Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
+  iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as (v) "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
     wp_match. iApply ("IH" with "Hγ Hv").