diff --git a/Makefile b/Makefile
index 51cf12d0852549f11dde463406570900ee31d326..fa51a2f76603c5121c6817f59fc307b8184c79ab 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,7 @@
 %: Makefile.coq phony
 	+@make -f Makefile.coq $@
 
+# Compile this project
 all: Makefile.coq
 	+@make -f Makefile.coq all
 
@@ -11,11 +12,13 @@ clean: Makefile.coq
 Makefile.coq: _CoqProject Makefile
 	coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
 
-iris-local: clean
-	git submodule update --init iris
-	ln -nsf iris iris-enabled
-	+make -C iris -f Makefile
+# Use local Iris dependency
+iris-local:
+	git submodule update --init iris # If not initialized, then initialize; If not updated with this remote, then update
+	ln -nsf iris iris-enabled # If not linked, then link
+	+make -C iris -f Makefile # If not built, then build
 
+# Use system-installed Iris dependency
 iris-system: clean
 	rm -f iris-enabled
 
diff --git a/README.md b/README.md
index a83b6ccd6dd243b1bda8752055ae6cc1df4e9c68..d313458f637f247b91bee6670a8d1043e0659d11 100644
--- a/README.md
+++ b/README.md
@@ -24,3 +24,7 @@ version), run `make iris-local`.  Run this command again later to update the
 local Iris, in case the preferred Iris version changed.
 
 Now run `make` to build the full development.
+
+## Update local dependency by tracking Iris `master`
+
+   git submodule update --remote
diff --git a/iris b/iris
index 6cb76aaaf15d46c74c2a779f1e4e1ca1a53c0838..e3cb5b14e01ac2b349516f084e7def4bf7283ab9 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit 6cb76aaaf15d46c74c2a779f1e4e1ca1a53c0838
+Subproject commit e3cb5b14e01ac2b349516f084e7def4bf7283ab9
diff --git a/theories/atomic.v b/theories/atomic.v
index be3168a8b4d0952d4d4b3a0c369fc4dfe912bb99..84ddd9a335cfb8c11191765a8b7e7a41c5b8e44a 100644
--- a/theories/atomic.v
+++ b/theories/atomic.v
@@ -16,8 +16,8 @@ Section atomic.
              (Ei Eo: coPset) (* inside/outside masks *)
              (e: expr _) : iProp Σ :=
     (∀ P Q, (P ={Eo, Ei}=> ∃ x:A,
-                       α x ★
-                       ((α x ={Ei, Eo}=★ P) ∧
-                        (∀ v, β x v ={Ei, Eo}=★ Q v))
-     ) -★ {{ P }} e @ ⊤ {{ Q }})%I.
+                       α x ∗
+                       ((α x ={Ei, Eo}=∗ P) ∧
+                        (∀ v, β x v ={Ei, Eo}=∗ Q v))
+     ) -∗ {{ P }} e @ ⊤ {{ Q }})%I.
 End atomic.
diff --git a/theories/atomic_incr.v b/theories/atomic_incr.v
index 6e5dbba04034890dba2a460344dc34dc0f27f4e4..0b408dad547348154d45f9f132bc2d702cc6dcb7 100644
--- a/theories/atomic_incr.v
+++ b/theories/atomic_incr.v
@@ -20,7 +20,7 @@ Section incr.
   (* TODO: Can we have a more WP-style definition and avoid the equality? *)
   Definition incr_triple (l: loc) :=
     atomic_triple (fun (v: Z) => l ↦ #v)%I
-                  (fun v ret => ret = #v ★ l ↦ #(v + 1))%I
+                  (fun v ret => ret = #v ∗ l ↦ #(v + 1))%I
                   (nclose heapN)
                   ⊤
                   (incr #l).
@@ -61,7 +61,7 @@ Section user.
   Definition incr_2 : val :=
     λ: "x",
        let: "l" := ref "x" in
-       incr "l" || incr "l";;
+       incr "l" ||| incr "l";;
        !"l".
 
   (* prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *)
@@ -74,8 +74,8 @@ Section user.
     wp_alloc l as "Hl".
     iMod (inv_alloc N _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
     wp_let.
-    wp_bind (_ || _)%E.
-    iApply (wp_par (λ _, True%I) (λ _, True%I)).
+    wp_bind (_ ||| _)%E.
+    iApply (wp_par (λ _, True%I) (λ _, True%I) with "[]").
     iFrame "Hh".
     (* prove worker triple *)
     iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//.
diff --git a/theories/atomic_pcas.v b/theories/atomic_pcas.v
index 4b6b397ec66695b6acd750a9abcf1275b99df933..0319265b2ad213b1ef76a933086c22e51ca3917c 100644
--- a/theories/atomic_pcas.v
+++ b/theories/atomic_pcas.v
@@ -23,7 +23,7 @@ Section atomic_pair.
   
   Definition ϕ (ls: val) (xs: val) : iProp Σ :=
     (∃ (l1 l2: loc) (x1 x2: val),
-       ls = (#l1, #l2)%V ★ xs = (x1, x2)%V ★ l1 ↦ x1 ★ l2 ↦ x2)%I.
+       ls = (#l1, #l2)%V ∗ xs = (x1, x2)%V ∗ l1 ↦ x1 ∗ l2 ↦ x2)%I.
 
   Definition β (ab: val) (xs xs': val) (v: val) : iProp Σ :=
     (■ ∃ a b x1 x2 x1' x2': val,
@@ -69,8 +69,8 @@ Section atomic_pair.
 
   Lemma pcas_atomic_spec (mk_syncer: val) (l1 l2: loc) (x1 x2: val) :
     heapN ⊥ N → mk_syncer_spec N mk_syncer →
-    heap_ctx ★ l1 ↦ x1 ★ l2 ↦ x2
-    ⊢ WP sync mk_syncer pcas_seq (LitV l1, LitV l2)%V {{ f, ∃ γ, gHalf γ (x1, x2)%V ★ ∀ x, □ atomic_triple' α β ⊤ ⊤ f x γ  }}.
+    heap_ctx ∗ l1 ↦ x1 ∗ l2 ↦ x2
+    ⊢ WP sync mk_syncer pcas_seq (LitV l1, LitV l2)%V {{ f, ∃ γ, gHalf γ (x1, x2)%V ∗ ∀ x, □ atomic_triple' α β ⊤ ⊤ f x γ  }}.
   Proof.
     iIntros (HN Hmk_syncer) "(#Hh & Hl1 & Hl2)".
     iDestruct (atomic_spec with "[Hl1 Hl2]") as "Hspec"=>//.
diff --git a/theories/atomic_sync.v b/theories/atomic_sync.v
index 02c6b22b0b35f9495b205cd6e6d8079ca36604ff..189924157b8e06994b1fdc990c40692f750b7845 100644
--- a/theories/atomic_sync.v
+++ b/theories/atomic_sync.v
@@ -20,13 +20,13 @@ Section atomic_sync.
   Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, DecAgree g).
 
   Definition atomic_seq_spec (ϕ: A → iProp Σ) α β (f x: val) :=
-    (∀ g, {{ ϕ g ★ α g }} f x {{ v, ∃ g', ϕ g' ★ β g g' v }})%I.
+    (∀ g, {{ ϕ g ∗ α g }} f x {{ v, ∃ g', ϕ g' ∗ β g g' v }})%I.
 
   (* TODO: Provide better masks. ∅ as inner mask is pretty weak. *)
   Definition atomic_synced (ϕ: A → iProp Σ) γ (f f': val) :=
     (□ ∀ α β (x: val), atomic_seq_spec ϕ α β f x →
-                       atomic_triple (fun g => gHalf γ g ★ □ α g)%I
-                                     (fun g v => ∃ g', gHalf γ g' ★ β g g' v)%I
+                       atomic_triple (fun g => gHalf γ g ∗ □ α g)%I
+                                     (fun g v => ∃ g', gHalf γ g' ∗ β g g' v)%I
                                      ∅ ⊤ (f' x))%I.
 
   (* TODO: Use our usual style with a generic post-condition. *)
@@ -42,7 +42,7 @@ Section atomic_sync.
   Definition atomic_syncer_spec (mk_syncer: val) :=
     ∀ (g0: A) (ϕ: A → iProp Σ),
       heapN ⊥ N →
-      {{{ heap_ctx ★ ϕ g0 }}} mk_syncer #() {{{ γ s, RET s; gHalf γ g0 ★ is_atomic_syncer ϕ γ s }}}.
+      {{{ heap_ctx ∗ ϕ g0 }}} mk_syncer #() {{{ γ s, RET s; gHalf γ g0 ∗ is_atomic_syncer ϕ γ s }}}.
 
   Lemma atomic_spec (mk_syncer: val):
       mk_syncer_spec N mk_syncer → atomic_syncer_spec mk_syncer.
@@ -50,7 +50,7 @@ Section atomic_sync.
     iIntros (Hsync g0 Ï• HN ret) "[#Hh HÏ•] Hret".
     iMod (own_alloc (((1 / 2)%Qp, DecAgree g0) ⋅ ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]".
     { by rewrite pair_op dec_agree_idemp. }
-    iApply (Hsync (∃ g: A, ϕ g ★ gHalf γ g)%I with "[$Hh Hg1 Hϕ]")=>//.
+    iApply (Hsync (∃ g: A, ϕ g ∗ gHalf γ g)%I with "[$Hh Hg1 Hϕ]")=>//.
     { iExists g0. by iFrame. }
     iNext. iIntros (s) "#Hsyncer". iApply "Hret".
     iSplitL "Hg2"; first done. iIntros "!#".
diff --git a/theories/evmap.v b/theories/evmap.v
index 8010da28badb71b701077e5e3d8d1b1386e88bfc..0a27e63ec8f101d9d242b950e0081eee503a6186 100644
--- a/theories/evmap.v
+++ b/theories/evmap.v
@@ -69,7 +69,7 @@ Section evmapR.
   (* Some other supporting lemmas *)
   Lemma map_agree_none' γm (m: evmapR K A unitR) hd x:
     m !! hd = None →
-    own γm (● m) ★ ev γm hd x ⊢ False.
+    own γm (● m) ∗ ev γm hd x ⊢ False.
   Proof.
     iIntros (?) "[Hom Hev]".
     iCombine "Hom" "Hev" as "Hauth".
@@ -80,7 +80,7 @@ Section evmapR.
 
   Lemma map_agree_eq' γm m hd x agy:
     m !! hd = Some ((), agy) →
-    ev γm hd x ★ own γm (● m) ⊢ DecAgree x = agy.
+    ev γm hd x ∗ own γm (● m) ⊢ DecAgree x = agy.
   Proof.
     iIntros (?) "[#Hev Hom]".
     iCombine "Hom" "Hev" as "Hauth".
@@ -99,7 +99,7 @@ Section evmapR.
 
   (* Evidence is the witness of membership *)
   Lemma ev_map_witness γm m hd x:
-    ev γm hd x ★ own γm (● m) ⊢ m !! hd = Some (∅, DecAgree x).
+    ev γm hd x ∗ own γm (● m) ⊢ m !! hd = Some (∅, DecAgree x).
   Proof.
     iIntros "[#Hev Hom]".
     destruct (m !! hd) as [[[] agy]|] eqn:Heqn.
@@ -109,7 +109,7 @@ Section evmapR.
   
   (* Two evidences coincides *)
   Lemma evmap_frag_agree_split γm p (a1 a2: A):
-    ev γm p a1 ★ ev γm p a2 ⊢ a1 = a2.
+    ev γm p a1 ∗ ev γm p a2 ⊢ a1 = a2.
   Proof.
     iIntros "[Ho Ho']".
     destruct (decide (a1 = a2)) as [->|Hneq].
diff --git a/theories/flat.v b/theories/flat.v
index c7d587777b944aefc417fa5f6f3e222e988958a5..e9d112abae3c13d039e2ae0fa97ddec13da0475d 100644
--- a/theories/flat.v
+++ b/theories/flat.v
@@ -71,55 +71,55 @@ Section proof.
   Context `{!heapG Σ, !lockG Σ, !evidenceG loc val unitR Σ, !flatG Σ} (N : namespace).
 
   Definition init_s (ts: toks) :=
-    let '(_, γ1, γ3, _, _) := ts in (own γ1 (Excl ()) ★ own γ3 (Excl ()))%I.
+    let '(_, γ1, γ3, _, _) := ts in (own γ1 (Excl ()) ∗ own γ3 (Excl ()))%I.
 
   Definition installed_s R (ts: toks) (f x: val) :=
     let '(γx, γ1, _, γ4, γq) := ts in
     (∃ (P: val → iProp Σ) Q,
-       own γx ((1/2)%Qp, DecAgree x) ★ P x ★ ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) ★
-       saved_prop_own γq (Q x) ★ own γ1 (Excl ()) ★ own γ4 (Excl ()))%I.
+       own γx ((1/2)%Qp, DecAgree x) ∗ P x ∗ ({{ R ∗ P x }} f x {{ v, R ∗ Q x v }}) ∗
+       saved_prop_own γq (Q x) ∗ own γ1 (Excl ()) ∗ own γ4 (Excl ()))%I.
 
   Definition received_s (ts: toks) (x: val) γr :=
     let '(γx, _, _, γ4, _) := ts in
-    (own γx ((1/2/2)%Qp, DecAgree x) ★ own γr (Excl ()) ★ own γ4 (Excl ()))%I.
+    (own γx ((1/2/2)%Qp, DecAgree x) ∗ own γr (Excl ()) ∗ own γ4 (Excl ()))%I.
 
   Definition finished_s (ts: toks) (x y: val) :=
     let '(γx, γ1, _, γ4, γq) := ts in
     (∃ Q: val → val → iProp Σ,
-       own γx ((1/2)%Qp, DecAgree x) ★ saved_prop_own γq (Q x) ★
-       Q x y ★ own γ1 (Excl ()) ★ own γ4 (Excl ()))%I.
+       own γx ((1/2)%Qp, DecAgree x) ∗ saved_prop_own γq (Q x) ∗
+       Q x y ∗ own γ1 (Excl ()) ∗ own γ4 (Excl ()))%I.
 
   Definition evm := ev loc toks.
   
   (* p slot invariant *)
   Definition p_inv R (γm γr: gname) (v: val) :=
     (∃ (ts: toks) (p : loc),
-       v = #p ★ evm γm p ts ★
+       v = #p ∗ evm γm p ts ∗
        ((* INIT *)
-        (∃ y: val, p ↦{1/2} InjRV y ★ init_s ts)∨
+        (∃ y: val, p ↦{1/2} InjRV y ∗ init_s ts)∨
         (* INSTALLED *)
-        (∃ f x: val, p ↦{1/2} InjLV (f, x) ★ installed_s R ts f x) ∨
+        (∃ f x: val, p ↦{1/2} InjLV (f, x) ∗ installed_s R ts f x) ∨
         (* RECEIVED *)
-        (∃ f x: val, p ↦{1/2} InjLV (f, x) ★ received_s ts x γr) ∨
+        (∃ f x: val, p ↦{1/2} InjLV (f, x) ∗ received_s ts x γr) ∨
         (* FINISHED *)
-        (∃ x y: val, p ↦{1/2} InjRV y ★ finished_s ts x y)))%I.
+        (∃ x y: val, p ↦{1/2} InjRV y ∗ finished_s ts x y)))%I.
 
   Definition srv_stack_inv R γs γm γr s := (∃ xs, is_stack' (p_inv R γm γr) γs xs s)%I.
 
-  Definition srv_tokm_inv γm := (∃ m : tokmR, own γm (● m) ★ [★ map] p ↦ _ ∈ m, ∃ v, p ↦{1/2} v)%I.
+  Definition srv_tokm_inv γm := (∃ m : tokmR, own γm (● m) ∗ [∗ map] p ↦ _ ∈ m, ∃ v, p ↦{1/2} v)%I.
 
   Lemma install_push_spec R
         (p: loc) (γs γm γr: gname) (ts: toks)
         (s: loc) (f x: val) (Φ: val → iProp Σ) :
     heapN ⊥ N →
-    heap_ctx ★ inv N (srv_stack_inv R γs γm γr s ★ srv_tokm_inv γm) ★
-    evm γm p ts ★ installed_s R ts f x ★
-    p ↦{1/2} InjLV (f, x) ★ ((∃ hd, evs γs hd #p) -★ Φ #())
+    heap_ctx ∗ inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗
+    evm γm p ts ∗ installed_s R ts f x ∗
+    p ↦{1/2} InjLV (f, x) ∗ ((∃ hd, evs γs hd #p) -∗ Φ #())
     ⊢ WP push #s #p {{ Φ }}.
   Proof.
     iIntros (HN) "(#Hh & #? & Hpm & Hs & Hp & HΦ)".
     rewrite /srv_stack_inv.
-    iDestruct (push_spec N (p_inv R γm γr) (fun v => (∃ hd, evs γs hd #p) ★ v = #())%I
+    iDestruct (push_spec N (p_inv R γm γr) (fun v => (∃ hd, evs γs hd #p) ∗ v = #())%I
                with "[-HΦ]") as "Hpush"=>//.
     - iFrame "Hh". iSplitL "Hp Hs Hpm"; last eauto.
       iExists ts. iExists p. iSplit=>//. iFrame "Hpm".
@@ -132,16 +132,16 @@ Section proof.
 
   Definition installed_recp (ts: toks) (x: val) (Q: val → iProp Σ) :=
     let '(γx, _, γ3, _, γq) := ts in
-    (own γ3 (Excl ()) ★ own γx ((1/2)%Qp, DecAgree x) ★ saved_prop_own γq Q)%I.
+    (own γ3 (Excl ()) ∗ own γx ((1/2)%Qp, DecAgree x) ∗ saved_prop_own γq Q)%I.
 
   Lemma install_spec
         R P Q
         (f x: val) (γs γm γr: gname) (s: loc)
         (Φ: val → iProp Σ):
     heapN ⊥ N →
-    heap_ctx ★ inv N (srv_stack_inv R γs γm γr s ★ srv_tokm_inv γm) ★
-    P ★ ({{ R ★ P }} f x {{ v, R ★ Q v }}) ★
-    (∀ (p: loc) (ts: toks), installed_recp ts x Q -★ evm γm p ts -★(∃ hd, evs γs hd #p) -★ Φ #p)
+    heap_ctx ∗ inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗
+    P ∗ ({{ R ∗ P }} f x {{ v, R ∗ Q v }}) ∗
+    (∀ (p: loc) (ts: toks), installed_recp ts x Q -∗ evm γm p ts -∗(∃ hd, evs γs hd #p) -∗ Φ #p)
     ⊢ WP install f x #s {{ Φ }}.
   Proof.
     iIntros (HN) "(#Hh & #? & Hpx & Hf & HΦ)".
@@ -181,14 +181,14 @@ Section proof.
 
   Lemma loop_iter_doOp_spec R (s hd: loc) (γs γm γr: gname) xs Φ:
     heapN ⊥ N →
-    heap_ctx ★ inv N (srv_stack_inv R γs γm γr s ★ srv_tokm_inv γm) ★ own γr (Excl ()) ★ R ★
-    is_list' γs hd xs ★ (own γr (Excl ()) -★ R -★ Φ #())
+    heap_ctx ∗ inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗ own γr (Excl ()) ∗ R ∗
+    is_list' γs hd xs ∗ (own γr (Excl ()) -∗ R -∗ Φ #())
     ⊢ WP iter #hd doOp {{ Φ }}.
   Proof.
     iIntros (HN) "(#Hf & #? & Ho2 & HR & Hlist' & HΦ)".
     iApply (iter_spec N (p_inv R γm γr) Φ
-                      (* (fun v => v = #() ★ own γr (Excl ()) ★ R)%I *)
-                      γs s (own γr (Excl ()) ★ R)%I (srv_tokm_inv γm) xs hd doOp doOp
+                      (* (fun v => v = #() ∗ own γr (Excl ()) ∗ R)%I *)
+                      γs s (own γr (Excl ()) ∗ R)%I (srv_tokm_inv γm) xs hd doOp doOp
             with "[-]")=>//.
     - rewrite /f_spec.
       iIntros (Φ' x _) "(#Hh & #? & Hev & [Hor HR] & HΦ')".
@@ -296,12 +296,12 @@ Section proof.
   Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
   Definition finished_recp (ts: toks) (x y: val) :=
     let '(γx, _, _, _, γq) := ts in
-    (∃ Q, own γx ((1 / 2)%Qp, DecAgree x) ★ saved_prop_own γq (Q x) ★ Q x y)%I.
+    (∃ Q, own γx ((1 / 2)%Qp, DecAgree x) ∗ saved_prop_own γq (Q x) ∗ Q x y)%I.
 
   Lemma try_srv_spec R (s: loc) (lk: val) (γs γr γm γlk: gname) Φ :
     heapN ⊥ N →
-    heap_ctx ★ inv N (srv_stack_inv R γs γm γr s ★ srv_tokm_inv γm) ★
-    is_lock N γlk lk (own γr (Excl ()) ★ R) ★ Φ #()
+    heap_ctx ∗ inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗
+    is_lock N γlk lk (own γr (Excl ()) ∗ R) ∗ Φ #()
     ⊢ WP try_srv lk #s {{ Φ }}.
   Proof.
     iIntros (?) "(#? & #? & #? & HΦ)".
@@ -319,20 +319,20 @@ Section proof.
     iModIntro. wp_let.
     wp_bind (iter _ _).
     iApply wp_wand_r. iSplitL "HR Ho2 Hxs2".
-    { iApply (loop_iter_doOp_spec R _ _ _ _ _ _ (fun v => own γr (Excl ()) ★ R ★ v = #()))%I=>//.      
+    { iApply (loop_iter_doOp_spec R _ _ _ _ _ _ (fun v => own γr (Excl ()) ∗ R ∗ v = #()))%I=>//.      
       iFrame "#". iFrame. iIntros "? ?". by iFrame. }
     iIntros (f') "[Ho [HR %]]". subst.
-    wp_let. iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#★".
+    wp_let. iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#∗".
     iNext. iIntros. done.
   Qed.
 
   Lemma loop_spec R (p s: loc) (lk: val)
         (γs γr γm γlk: gname) (ts: toks) Φ:
     heapN ⊥ N →
-    heap_ctx ★ inv N (srv_stack_inv R γs γm γr s ★ srv_tokm_inv γm) ★
-    is_lock N γlk lk (own γr (Excl ()) ★ R) ★
-    own_γ3 ts ★ evm γm p ts ★
-    (∃ hd, evs γs hd #p) ★ (∀ x y, finished_recp ts x y -★ Φ y)
+    heap_ctx ∗ inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗
+    is_lock N γlk lk (own γr (Excl ()) ∗ R) ∗
+    own_γ3 ts ∗ evm γm p ts ∗
+    (∃ hd, evs γs hd #p) ∗ (∀ x y, finished_recp ts x y -∗ Φ y)
     ⊢ WP loop #p #s lk {{ Φ }}.
   Proof.
     iIntros (HN) "(#Hh & #? & #? & Ho3 & #Hev & Hhd & HΦ)".
@@ -398,7 +398,7 @@ Section proof.
     iAssert (srv_tokm_inv γm) with "[Hm]" as "Hm"; first eauto.
     { iExists ∅. iFrame. by rewrite big_sepM_empty. }
     wp_seq. wp_bind (newlock _).
-    iApply (newlock_spec _ (own γr (Excl ()) ★ R)%I with "[$Hh $Ho2 $HR]")=>//.
+    iApply (newlock_spec _ (own γr (Excl ()) ∗ R)%I with "[$Hh $Ho2 $HR]")=>//.
     iNext. iIntros (lk γlk) "#Hlk".
     wp_let. wp_bind (new_stack _).
     iApply (new_stack_spec' _ (p_inv _ γm γr))=>//.
diff --git a/theories/misc.v b/theories/misc.v
index 0a559fd772ff3744ad23875a3540da27bcd22fd0..bb5703461ba386eb10e18a8d741f3dc95e43198c 100644
--- a/theories/misc.v
+++ b/theories/misc.v
@@ -21,7 +21,7 @@ End lemmas.
 Section excl.
   Context `{!inG Σ (exclR unitC)}.
   Lemma excl_falso γ Q':
-    own γ (Excl ()) ★ own γ (Excl ()) ⊢ Q'.
+    own γ (Excl ()) ∗ own γ (Excl ()) ⊢ Q'.
   Proof.
     iIntros "[Ho1 Ho2]". iCombine "Ho1" "Ho2" as "Ho".
     iExFalso. by iDestruct (own_valid with "Ho") as "%".
@@ -33,7 +33,7 @@ Section heap_extra.
 
   Lemma bogus_heap p (q1 q2: Qp) a b:
     ~((q1 + q2)%Qp ≤ 1%Qp)%Qc →
-    heap_ctx ★ p ↦{q1} a ★ p ↦{q2} b ⊢ False.
+    heap_ctx ∗ p ↦{q1} a ∗ p ↦{q2} b ⊢ False.
   Proof.
     iIntros (?) "(#Hh & Hp1 & Hp2)".
     iCombine "Hp1" "Hp2" as "Hp".
@@ -52,12 +52,12 @@ Section big_op_later.
 
   Lemma big_sepM_delete_later Φ m i x :
     m !! i = Some x →
-    ▷ ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ ▷ Φ i x ★ ▷ [★ map] k↦y ∈ delete i m, Φ k y.
+    ▷ ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ ▷ Φ i x ∗ ▷ [∗ map] k↦y ∈ delete i m, Φ k y.
   Proof. intros ?. rewrite big_sepM_delete=>//. apply later_sep. Qed.
 
   Lemma big_sepM_insert_later Φ m i x :
     m !! i = None →
-    ▷ ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ ▷ Φ i x ★ ▷ [★ map] k↦y ∈ m, Φ k y.
+    ▷ ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ ▷ Φ i x ∗ ▷ [∗ map] k↦y ∈ m, Φ k y.
   Proof. intros ?. rewrite big_sepM_insert=>//. apply later_sep. Qed.
 End big_op_later.
 
@@ -65,7 +65,7 @@ Section pair.
   Context `{EqDecision A, !inG Σ (prodR fracR (dec_agreeR A))}.
 
   Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A):
-    own γm (q1, DecAgree a1) ★ own γm (q2, DecAgree a2) ⊢ (a1 = a2).
+    own γm (q1, DecAgree a1) ∗ own γm (q2, DecAgree a2) ⊢ (a1 = a2).
   Proof.
     iIntros "[Ho Ho']".
     destruct (decide (a1 = a2)) as [->|Hneq]=>//.
@@ -76,8 +76,8 @@ Section pair.
   Qed.
   
   Lemma m_frag_agree' γm (q1 q2: Qp) (a1 a2: A):
-    own γm (q1, DecAgree a1) ★ own γm (q2, DecAgree a2)
-    ⊢ own γm ((q1 + q2)%Qp, DecAgree a1) ★ (a1 = a2).
+    own γm (q1, DecAgree a1) ∗ own γm (q2, DecAgree a2)
+    ⊢ own γm ((q1 + q2)%Qp, DecAgree a1) ∗ (a1 = a2).
   Proof.
     iIntros "[Ho Ho']".
     iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame.
diff --git a/theories/peritem.v b/theories/peritem.v
index ce12b4741d39325b14b116e7a21cf689b32bbf3a..c86c94fe1a69b4b28ea6b33001b5e6379fbb9a9e 100644
--- a/theories/peritem.v
+++ b/theories/peritem.v
@@ -16,13 +16,13 @@ Section defs.
   Fixpoint is_list' (γ: gname) (hd: loc) (xs: list val) : iProp Σ :=
     match xs with
     | [] => (∃ q, hd ↦{ q } NONEV)%I
-    | x :: xs => (∃ (hd': loc) q, hd ↦{q} SOMEV (x, #hd') ★ evs γ hd x ★ is_list' γ hd' xs)%I
+    | x :: xs => (∃ (hd': loc) q, hd ↦{q} SOMEV (x, #hd') ∗ evs γ hd x ∗ is_list' γ hd' xs)%I
     end.
 
   Lemma in_list' γ x xs:
     ∀ hd, x ∈ xs →
           is_list' γ hd xs
-          ⊢ ∃ (hd' hd'': loc) q, hd' ↦{q} SOMEV (x, #hd'') ★ evs γ hd' x.
+          ⊢ ∃ (hd' hd'': loc) q, hd' ↦{q} SOMEV (x, #hd'') ∗ evs γ hd' x.
   Proof.
     induction xs as [|x' xs' IHxs'].
     - intros ? Hin. inversion Hin.
@@ -36,13 +36,13 @@ Section defs.
         iApply IHxs'=>//.
   Qed.
 
-  Definition perR' hd v v' := (v = ((∅: unitR), DecAgree v') ★ R v' ★ allocated hd)%I.
+  Definition perR' hd v v' := (v = ((∅: unitR), DecAgree v') ∗ R v' ∗ allocated hd)%I.
   Definition perR  hd v := (∃ v', perR' hd v v')%I.
   
-  Definition allR γ := (∃ m : evmapR loc val unitR, own γ (● m) ★ [★ map] hd ↦ v ∈ m, perR hd v)%I.
+  Definition allR γ := (∃ m : evmapR loc val unitR, own γ (● m) ∗ [∗ map] hd ↦ v ∈ m, perR hd v)%I.
 
   Definition is_stack' γ xs s :=
-    (∃ hd: loc, s ↦ #hd ★ is_list' γ hd xs ★ allR γ)%I.
+    (∃ hd: loc, s ↦ #hd ∗ is_list' γ hd xs ∗ allR γ)%I.
 
   Global Instance is_list'_timeless γ hd xs: TimelessP (is_list' γ hd xs).
   Proof. generalize hd. induction xs; apply _. Qed.
@@ -51,7 +51,7 @@ Section defs.
   Proof. apply _. Qed.
 
   Lemma dup_is_list' γ : ∀ xs hd,
-    heap_ctx ★ is_list' γ hd xs ⊢ |==> is_list' γ hd xs ★ is_list' γ hd xs.
+    heap_ctx ∗ is_list' γ hd xs ⊢ |==> is_list' γ hd xs ∗ is_list' γ hd xs.
   Proof.
     induction xs as [|y xs' IHxs'].
     - iIntros (hd) "(#? & Hs)".
@@ -63,7 +63,7 @@ Section defs.
   Qed.
 
   Lemma extract_is_list γ : ∀ xs hd,
-    heap_ctx ★ is_list' γ hd xs ⊢ |==> is_list' γ hd xs ★ is_list hd xs.
+    heap_ctx ∗ is_list' γ hd xs ⊢ |==> is_list' γ hd xs ∗ is_list hd xs.
   Proof.
     induction xs as [|y xs' IHxs'].
     - iIntros (hd) "(#? & Hs)".
@@ -78,8 +78,8 @@ Section defs.
     (* Rf, RI is some frame *)
     ∀ Φ (x: val),
       heapN ⊥ N →
-      heap_ctx ★ inv N ((∃ xs, is_stack' γ xs s) ★ RI) ★ (∃ hd, evs γ hd x) ★
-      Rf ★ (Rf -★ Φ #())
+      heap_ctx ∗ inv N ((∃ xs, is_stack' γ xs s) ∗ RI) ∗ (∃ hd, evs γ hd x) ∗
+      Rf ∗ (Rf -∗ Φ #())
       ⊢ WP f x {{ Φ }}.
 End defs.
 
@@ -89,7 +89,7 @@ Section proofs.
 
 Lemma new_stack_spec' Φ RI:
     heapN ⊥ N →
-    heap_ctx ★ RI ★ (∀ γ s : loc, inv N ((∃ xs, is_stack' R γ xs s) ★ RI) -★ Φ #s)
+    heap_ctx ∗ RI ∗ (∀ γ s : loc, inv N ((∃ xs, is_stack' R γ xs s) ∗ RI) -∗ Φ #s)
     ⊢ WP new_stack #() {{ Φ }}.
   Proof.
     iIntros (HN) "(#Hh & HR & HΦ)". iApply wp_fupd.
@@ -97,19 +97,19 @@ Lemma new_stack_spec' Φ RI:
     { apply auth_valid_discrete_2. done. }
     wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
     wp_alloc s as "Hs".
-    iAssert ((∃ xs : list val, is_stack' R γ xs s) ★ RI)%I with "[-HΦ Hm']" as "Hinv".
+    iAssert ((∃ xs : list val, is_stack' R γ xs s) ∗ RI)%I with "[-HΦ Hm']" as "Hinv".
     { iFrame. iExists [], l. iFrame. simpl. iSplitL "Hl".
       - eauto.
       - iExists ∅. iSplitL. iFrame. by iApply (big_sepM_empty (fun hd v => perR R hd v)). }
-    iMod (inv_alloc N _ ((∃ xs : list val, is_stack' R γ xs s) ★ RI)%I with "[-HΦ Hm']") as "#?"; first eauto.
+    iMod (inv_alloc N _ ((∃ xs : list val, is_stack' R γ xs s) ∗ RI)%I with "[-HΦ Hm']") as "#?"; first eauto.
     by iApply "HΦ".
   Qed.
     
   Lemma iter_spec Φ γ s (Rf RI: iProp Σ):
     ∀ xs hd (f: expr) (f': val),
       heapN ⊥ N → f_spec N R γ xs s f' Rf RI → to_val f = Some f' →
-      heap_ctx ★ inv N ((∃ xs, is_stack' R γ xs s) ★ RI) ★
-      is_list' γ hd xs ★ Rf ★ (Rf -★ Φ #())
+      heap_ctx ∗ inv N ((∃ xs, is_stack' R γ xs s) ∗ RI) ∗
+      is_list' γ hd xs ∗ Rf ∗ (Rf -∗ Φ #())
       ⊢ WP (iter #hd) f {{ v, Φ v }}.
   Proof.
     induction xs as [|x xs' IHxs'].
@@ -128,12 +128,12 @@ Lemma new_stack_spec' Φ RI:
   
   Lemma push_spec Φ γ (s: loc) (x: val) RI:
     heapN ⊥ N →
-    heap_ctx ★ R x ★ inv N ((∃ xs, is_stack' R γ xs s) ★ RI) ★ ((∃ hd, evs γ hd x) -★ Φ #())
+    heap_ctx ∗ R x ∗ inv N ((∃ xs, is_stack' R γ xs s) ∗ RI) ∗ ((∃ hd, evs γ hd x) -∗ Φ #())
     ⊢ WP push #s x {{ Φ }}.
   Proof.
     iIntros (HN) "(#Hh & HRx & #? & HΦ)".
     iDestruct (push_atomic_spec N s x with "Hh") as "Hpush"=>//.
-    iSpecialize ("Hpush" $! (R x) (fun ret => (∃ hd, evs γ hd x) ★ ret = #())%I with "[]").
+    iSpecialize ("Hpush" $! (R x) (fun ret => (∃ hd, evs γ hd x) ∗ ret = #())%I with "[]").
     - iIntros "!# Rx".
       (* open the invariant *)
       iInv N as "[IH1 ?]" "Hclose".
@@ -161,7 +161,7 @@ Lemma new_stack_spec' Φ RI:
           iDestruct "Hhd''" as (q v) "Hhd''". iExFalso.
           iApply (bogus_heap hd' 1%Qp q); first apply Qp_not_plus_q_ge_1.
           iFrame "#". iFrame.
-        * iAssert (evs γ hd' x ★ ▷ (allR R γ))%I
+        * iAssert (evs γ hd' x ∗ ▷ (allR R γ))%I
                   with ">[Rx Hom HRm Hhd'1]" as "[#Hox ?]".
           {
             iDestruct (evmap_alloc _ _ _ m with "[Hom]") as ">[Hom Hox]"=>//.
diff --git a/theories/sync.v b/theories/sync.v
index 9de76b8e5e0e112e4090cdd60ada784109714c09..de42cf6c654cdf5fbd80a2609da7a72a8d500fea 100644
--- a/theories/sync.v
+++ b/theories/sync.v
@@ -12,7 +12,7 @@ Section sync.
      How much more annoying? And how much to we gain in terms of things
      becomign easier to prove? *)
   Definition synced R (f f': val) :=
-    (□ ∀ P Q (x: val), {{ R ★ P }} f x {{ v, R ★ Q v }} →
+    (□ ∀ P Q (x: val), {{ R ∗ P }} f x {{ v, R ∗ Q v }} →
                        {{ P }} f' x {{ Q }})%I.
 
   (* Notice that `s f` is *unconditionally safe* to execute, and only 
@@ -24,5 +24,5 @@ Section sync.
 
   Definition mk_syncer_spec (mk_syncer: val) :=
     ∀ (R: iProp Σ), heapN ⊥ N →
-      {{{ heap_ctx ★ R }}} mk_syncer #() {{{ s, RET s; is_syncer R s }}}.
+      {{{ heap_ctx ∗ R }}} mk_syncer #() {{{ s, RET s; is_syncer R s }}}.
 End sync.
diff --git a/theories/treiber.v b/theories/treiber.v
index 59c9b694dbb7944f28be746d33c4248cd87e74fe..bb356779cc6f24127763ceb9181af2149359d139 100644
--- a/theories/treiber.v
+++ b/theories/treiber.v
@@ -41,11 +41,11 @@ Section proof.
   Fixpoint is_list (hd: loc) (xs: list val) : iProp Σ :=
     match xs with
     | [] => (∃ q, hd ↦{ q } NONEV)%I
-    | x :: xs => (∃ (hd': loc) q, hd ↦{ q } SOMEV (x, #hd') ★ is_list hd' xs)%I
+    | x :: xs => (∃ (hd': loc) q, hd ↦{ q } SOMEV (x, #hd') ∗ is_list hd' xs)%I
     end.
 
   Lemma dup_is_list : ∀ xs hd,
-    heap_ctx ★ is_list hd xs ⊢ is_list hd xs ★ is_list hd xs.
+    heap_ctx ∗ is_list hd xs ⊢ is_list hd xs ∗ is_list hd xs.
   Proof.
     induction xs as [|y xs' IHxs'].
     - iIntros (hd) "(#? & Hs)".
@@ -57,7 +57,7 @@ Section proof.
   Qed.
 
   Lemma uniq_is_list:
-    ∀ xs ys hd, heap_ctx ★ is_list hd xs ★ is_list hd ys ⊢ xs = ys.
+    ∀ xs ys hd, heap_ctx ∗ is_list hd xs ∗ is_list hd ys ⊢ xs = ys.
   Proof.
     induction xs as [|x xs' IHxs'].
     - induction ys as [|y ys' IHys'].
@@ -86,7 +86,7 @@ Section proof.
         by subst.
   Qed.
 
-  Definition is_stack (s: loc) xs: iProp Σ := (∃ hd: loc, s ↦ #hd ★ is_list hd xs)%I.
+  Definition is_stack (s: loc) xs: iProp Σ := (∃ hd: loc, s ↦ #hd ∗ is_list hd xs)%I.
 
   Global Instance is_list_timeless xs hd: TimelessP (is_list hd xs).
   Proof. generalize hd. induction xs; apply _. Qed.
@@ -97,7 +97,7 @@ Section proof.
   Lemma new_stack_spec:
     ∀ (Φ: val → iProp Σ),
       heapN ⊥ N →
-      heap_ctx ★ (∀ s, is_stack s [] -★ Φ #s) ⊢ WP new_stack #() {{ Φ }}.
+      heap_ctx ∗ (∀ s, is_stack s [] -∗ Φ #s) ⊢ WP new_stack #() {{ Φ }}.
   Proof.
     iIntros (Φ HN) "[#Hh HΦ]". wp_seq.
     wp_bind (ref NONE)%E. wp_alloc l as "Hl".
@@ -108,11 +108,11 @@ Section proof.
 
   Definition push_triple (s: loc) (x: val) :=
   atomic_triple (fun xs_hd: list val * loc =>
-                     let '(xs, hd) := xs_hd in s ↦ #hd ★ is_list hd xs)%I
+                     let '(xs, hd) := xs_hd in s ↦ #hd ∗ is_list hd xs)%I
                 (fun xs_hd ret =>
                    let '(xs, hd) := xs_hd in 
                    ∃ hd': loc,
-                     ret = #() ★ s ↦ #hd' ★ hd' ↦ SOMEV (x, #hd) ★ is_list hd xs)%I
+                     ret = #() ∗ s ↦ #hd' ∗ hd' ↦ SOMEV (x, #hd) ∗ is_list hd xs)%I
                 (nclose heapN)
                 ⊤
                 (push #s x).
@@ -142,12 +142,12 @@ Section proof.
 
   Definition pop_triple (s: loc) :=
   atomic_triple (fun xs_hd: list val * loc =>
-                   let '(xs, hd) := xs_hd in s ↦ #hd ★ is_list hd xs)%I
+                   let '(xs, hd) := xs_hd in s ↦ #hd ∗ is_list hd xs)%I
                 (fun xs_hd ret =>
                    let '(xs, hd) := xs_hd in
-                   (ret = NONEV ★ xs = [] ★ s ↦ #hd ★ is_list hd []) ∨
-                   (∃ x q (hd': loc) xs', hd ↦{q} SOMEV (x, #hd') ★ ret = SOMEV x ★
-                                          xs = x :: xs' ★ s ↦ #hd' ★ is_list hd' xs'))%I
+                   (ret = NONEV ∗ xs = [] ∗ s ↦ #hd ∗ is_list hd []) ∨
+                   (∃ x q (hd': loc) xs', hd ↦{q} SOMEV (x, #hd') ∗ ret = SOMEV x ∗
+                                          xs = x :: xs' ∗ s ↦ #hd' ∗ is_list hd' xs'))%I
                 (nclose heapN)
                 ⊤
                 (pop #s).