Commit 6e487530 authored by Robbert Krebbers's avatar Robbert Krebbers

Explicit namespace for heap instead of parametrizing over it.

parent 2d44c0ef
...@@ -8,6 +8,7 @@ Import uPred. ...@@ -8,6 +8,7 @@ Import uPred.
a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
predicates over finmaps instead of just ownP. *) predicates over finmaps instead of just ownP. *)
Definition heapN : namespace := nroot .@ "heap".
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)). Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
(** The CMRA we need. *) (** The CMRA we need. *)
...@@ -22,7 +23,7 @@ Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)). ...@@ -22,7 +23,7 @@ Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)).
Definition of_heap : heapUR state := omap (maybe DecAgree snd). Definition of_heap : heapUR state := omap (maybe DecAgree snd).
Section definitions. Section definitions.
Context `{i : heapG Σ}. Context `{heapG Σ}.
Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iPropG heap_lang Σ := Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iPropG heap_lang Σ :=
auth_own heap_name {[ l := (q, DecAgree v) ]}. auth_own heap_name {[ l := (q, DecAgree v) ]}.
...@@ -33,12 +34,12 @@ Section definitions. ...@@ -33,12 +34,12 @@ Section definitions.
Definition heap_inv (h : heapUR) : iPropG heap_lang Σ := Definition heap_inv (h : heapUR) : iPropG heap_lang Σ :=
ownP (of_heap h). ownP (of_heap h).
Definition heap_ctx (N : namespace) : iPropG heap_lang Σ := Definition heap_ctx : iPropG heap_lang Σ :=
auth_ctx heap_name N heap_inv. auth_ctx heap_name heapN heap_inv.
Global Instance heap_inv_proper : Proper (() ==> (⊣⊢)) heap_inv. Global Instance heap_inv_proper : Proper (() ==> (⊣⊢)) heap_inv.
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance heap_ctx_persistent N : PersistentP (heap_ctx N). Global Instance heap_ctx_persistent : PersistentP heap_ctx.
Proof. apply _. Qed. Proof. apply _. Qed.
End definitions. End definitions.
...@@ -53,7 +54,6 @@ Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope. ...@@ -53,7 +54,6 @@ Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
Section heap. Section heap.
Context {Σ : gFunctors}. Context {Σ : gFunctors}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG heap_lang Σ. Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val iPropG heap_lang Σ. Implicit Types Φ : val iPropG heap_lang Σ.
Implicit Types σ : state. Implicit Types σ : state.
...@@ -103,13 +103,13 @@ Section heap. ...@@ -103,13 +103,13 @@ Section heap.
Hint Resolve heap_store_valid. Hint Resolve heap_store_valid.
(** Allocation *) (** Allocation *)
Lemma heap_alloc N E σ : Lemma heap_alloc E σ :
authG heap_lang Σ heapUR nclose N E authG heap_lang Σ heapUR nclose heapN E
ownP σ ={E}=> _ : heapG Σ, heap_ctx N [ map] lv σ, l v. ownP σ ={E}=> _ : heapG Σ, heap_ctx [ map] lv σ, l v.
Proof. Proof.
intros. rewrite -{1}(from_to_heap σ). etrans. intros. rewrite -{1}(from_to_heap σ). etrans.
{ rewrite [ownP _]later_intro. { rewrite [ownP _]later_intro.
apply (auth_alloc (ownP of_heap) N E); auto using to_heap_valid. } apply (auth_alloc (ownP of_heap) heapN E); auto using to_heap_valid. }
apply pvs_mono, exist_elim=> γ. apply pvs_mono, exist_elim=> γ.
rewrite -(exist_intro (HeapG _ _ γ)) /heap_ctx; apply and_mono_r. rewrite -(exist_intro (HeapG _ _ γ)) /heap_ctx; apply and_mono_r.
rewrite heap_mapsto_eq /heap_mapsto_def /heap_name. rewrite heap_mapsto_eq /heap_mapsto_def /heap_name.
...@@ -149,9 +149,9 @@ Section heap. ...@@ -149,9 +149,9 @@ Section heap.
(** Weakest precondition *) (** Weakest precondition *)
(* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *) (* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *)
Lemma wp_alloc N E e v Φ : Lemma wp_alloc E e v Φ :
to_val e = Some v nclose N E to_val e = Some v nclose heapN E
heap_ctx N ( l, l v ={E}= Φ (LitV (LitLoc l))) WP Alloc e @ E {{ Φ }}. heap_ctx ( l, l v ={E}= Φ (LitV (LitLoc l))) WP Alloc e @ E {{ Φ }}.
Proof. Proof.
iIntros (??) "[#Hinv HΦ]". rewrite /heap_ctx. iIntros (??) "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap". iPvs (auth_empty heap_name) as "Hheap".
...@@ -166,9 +166,9 @@ Section heap. ...@@ -166,9 +166,9 @@ Section heap.
iIntros "Hheap". iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def. iIntros "Hheap". iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
Qed. Qed.
Lemma wp_load N E l q v Φ : Lemma wp_load E l q v Φ :
nclose N E nclose heapN E
heap_ctx N l {q} v (l {q} v ={E}= Φ v) heap_ctx l {q} v (l {q} v ={E}= Φ v)
WP Load (Lit (LitLoc l)) @ E {{ Φ }}. WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof. Proof.
iIntros (?) "[#Hh [Hl HΦ]]". iIntros (?) "[#Hh [Hl HΦ]]".
...@@ -181,9 +181,9 @@ Section heap. ...@@ -181,9 +181,9 @@ Section heap.
rewrite of_heap_singleton_op //. by iFrame. rewrite of_heap_singleton_op //. by iFrame.
Qed. Qed.
Lemma wp_store N E l v' e v Φ : Lemma wp_store E l v' e v Φ :
to_val e = Some v nclose N E to_val e = Some v nclose heapN E
heap_ctx N l v' (l v ={E}= Φ (LitV LitUnit)) heap_ctx l v' (l v ={E}= Φ (LitV LitUnit))
WP Store (Lit (LitLoc l)) e @ E {{ Φ }}. WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof. Proof.
iIntros (??) "[#Hh [Hl HΦ]]". iIntros (??) "[#Hh [Hl HΦ]]".
...@@ -197,9 +197,9 @@ Section heap. ...@@ -197,9 +197,9 @@ Section heap.
rewrite of_heap_singleton_op //; eauto. by iFrame. rewrite of_heap_singleton_op //; eauto. by iFrame.
Qed. Qed.
Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 Φ : Lemma wp_cas_fail E l q v' e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 nclose N E to_val e1 = Some v1 to_val e2 = Some v2 v' v1 nclose heapN E
heap_ctx N l {q} v' (l {q} v' ={E}= Φ (LitV (LitBool false))) heap_ctx l {q} v' (l {q} v' ={E}= Φ (LitV (LitBool false)))
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}. WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof. Proof.
iIntros (????) "[#Hh [Hl HΦ]]". iIntros (????) "[#Hh [Hl HΦ]]".
...@@ -212,9 +212,9 @@ Section heap. ...@@ -212,9 +212,9 @@ Section heap.
rewrite of_heap_singleton_op //. by iFrame. rewrite of_heap_singleton_op //. by iFrame.
Qed. Qed.
Lemma wp_cas_suc N E l e1 v1 e2 v2 Φ : Lemma wp_cas_suc E l e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 nclose N E to_val e1 = Some v1 to_val e2 = Some v2 nclose heapN E
heap_ctx N l v1 (l v2 ={E}= Φ (LitV (LitBool true))) heap_ctx l v1 (l v2 ={E}= Φ (LitV (LitBool true)))
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}. WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof. Proof.
iIntros (???) "[#Hh [Hl HΦ]]". iIntros (???) "[#Hh [Hl HΦ]]".
......
...@@ -21,8 +21,7 @@ Proof. destruct H as (?&?&?). split; apply _. Qed. ...@@ -21,8 +21,7 @@ Proof. destruct H as (?&?&?). split; apply _. Qed.
(** Now we come to the Iris part of the proof. *) (** Now we come to the Iris part of the proof. *)
Section proof. Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ}. Context `{!heapG Σ, !barrierG Σ} (N : namespace).
Context (heapN N : namespace).
Implicit Types I : gset gname. Implicit Types I : gset gname.
Local Notation iProp := (iPropG heap_lang Σ). Local Notation iProp := (iPropG heap_lang Σ).
...@@ -42,7 +41,7 @@ Definition barrier_inv (l : loc) (P : iProp) (s : state) : iProp := ...@@ -42,7 +41,7 @@ Definition barrier_inv (l : loc) (P : iProp) (s : state) : iProp :=
(l s ress (state_to_prop s P) (state_I s))%I. (l s ress (state_to_prop s P) (state_I s))%I.
Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp := Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
( (heapN N) heap_ctx heapN sts_ctx γ N (barrier_inv l P))%I. ( (heapN N) heap_ctx sts_ctx γ N (barrier_inv l P))%I.
Definition send (l : loc) (P : iProp) : iProp := Definition send (l : loc) (P : iProp) : iProp :=
( γ, barrier_ctx γ l P sts_ownS γ low_states {[ Send ]})%I. ( γ, barrier_ctx γ l P sts_ownS γ low_states {[ Send ]})%I.
...@@ -96,8 +95,7 @@ Qed. ...@@ -96,8 +95,7 @@ Qed.
(** Actual proofs *) (** Actual proofs *)
Lemma newbarrier_spec (P : iProp) (Φ : val iProp) : Lemma newbarrier_spec (P : iProp) (Φ : val iProp) :
heapN N heapN N
heap_ctx heapN ( l, recv l P send l P - Φ #l) heap_ctx ( l, recv l P send l P - Φ #l) WP newbarrier #() {{ Φ }}.
WP newbarrier #() {{ Φ }}.
Proof. Proof.
iIntros (HN) "[#? HΦ]". iIntros (HN) "[#? HΦ]".
rewrite /newbarrier. wp_seq. wp_alloc l as "Hl". rewrite /newbarrier. wp_seq. wp_alloc l as "Hl".
......
...@@ -9,20 +9,20 @@ Context {Σ : gFunctors} `{!heapG Σ} `{!barrierG Σ}. ...@@ -9,20 +9,20 @@ Context {Σ : gFunctors} `{!heapG Σ} `{!barrierG Σ}.
Local Notation iProp := (iPropG heap_lang Σ). Local Notation iProp := (iPropG heap_lang Σ).
Lemma barrier_spec (heapN N : namespace) : Lemma barrier_spec (N : namespace) :
heapN N heapN N
recv send : loc iProp -n> iProp, recv send : loc iProp -n> iProp,
( P, heap_ctx heapN {{ True }} newbarrier #() {{ v, ( P, heap_ctx {{ True }} newbarrier #()
l : loc, v = #l recv l P send l P }}) {{ v, l : loc, v = #l recv l P send l P }})
( l P, {{ send l P P }} signal #l {{ _, True }}) ( l P, {{ send l P P }} signal #l {{ _, True }})
( l P, {{ recv l P }} wait #l {{ _, P }}) ( l P, {{ recv l P }} wait #l {{ _, P }})
( l P Q, recv l (P Q) ={N}=> recv l P recv l Q) ( l P Q, recv l (P Q) ={N}=> recv l P recv l Q)
( l P Q, (P - Q) recv l P - recv l Q). ( l P Q, (P - Q) recv l P - recv l Q).
Proof. Proof.
intros HN. intros HN.
exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)). exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
split_and?; simpl. split_and?; simpl.
- iIntros (P) "#? ! _". iApply (newbarrier_spec _ _ P); eauto. - iIntros (P) "#? ! _". iApply (newbarrier_spec _ P); eauto.
- iIntros (l P) "! [Hl HP]". by iApply signal_spec; iFrame "Hl HP". - iIntros (l P) "! [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
- iIntros (l P) "! Hl". iApply wait_spec; iFrame "Hl"; eauto. - iIntros (l P) "! Hl". iApply wait_spec; iFrame "Hl"; eauto.
- intros; by apply recv_split. - intros; by apply recv_split.
......
...@@ -20,14 +20,13 @@ Instance inGF_counterG `{H : inGFs heap_lang Σ counterGF} : counterG Σ. ...@@ -20,14 +20,13 @@ Instance inGF_counterG `{H : inGFs heap_lang Σ counterGF} : counterG Σ.
Proof. destruct H; split; apply _. Qed. Proof. destruct H; split; apply _. Qed.
Section proof. Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !counterG Σ}. Context `{!heapG Σ, !counterG Σ}.
Context (heapN : namespace).
Local Notation iProp := (iPropG heap_lang Σ). Local Notation iProp := (iPropG heap_lang Σ).
Definition counter_inv (l : loc) (n : mnat) : iProp := (l #n)%I. Definition counter_inv (l : loc) (n : mnat) : iProp := (l #n)%I.
Definition counter (l : loc) (n : nat) : iProp := Definition counter (l : loc) (n : nat) : iProp :=
( N γ, heapN N heap_ctx heapN ( N γ, heapN N heap_ctx
auth_ctx γ N (counter_inv l) auth_own γ (n:mnat))%I. auth_ctx γ N (counter_inv l) auth_own γ (n:mnat))%I.
(** The main proofs. *) (** The main proofs. *)
...@@ -36,7 +35,7 @@ Proof. apply _. Qed. ...@@ -36,7 +35,7 @@ Proof. apply _. Qed.
Lemma newcounter_spec N (R : iProp) Φ : Lemma newcounter_spec N (R : iProp) Φ :
heapN N heapN N
heap_ctx heapN ( l, counter l 0 - Φ #l) WP newcounter #() {{ Φ }}. heap_ctx ( l, counter l 0 - Φ #l) WP newcounter #() {{ Φ }}.
Proof. Proof.
iIntros (?) "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl". iIntros (?) "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
iPvs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]") iPvs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
......
...@@ -18,18 +18,17 @@ Instance inGF_lockG `{H : inGFs heap_lang Σ lockGF} : lockG Σ. ...@@ -18,18 +18,17 @@ Instance inGF_lockG `{H : inGFs heap_lang Σ lockGF} : lockG Σ.
Proof. destruct H. split. apply: inGF_inG. Qed. Proof. destruct H. split. apply: inGF_inG. Qed.
Section proof. Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !lockG Σ}. Context `{!heapG Σ, !lockG Σ}.
Context (heapN : namespace).
Local Notation iProp := (iPropG heap_lang Σ). Local Notation iProp := (iPropG heap_lang Σ).
Definition lock_inv (γ : gname) (l : loc) (R : iProp) : iProp := Definition lock_inv (γ : gname) (l : loc) (R : iProp) : iProp :=
( b : bool, l #b if b then True else own γ (Excl ()) R)%I. ( b : bool, l #b if b then True else own γ (Excl ()) R)%I.
Definition is_lock (l : loc) (R : iProp) : iProp := Definition is_lock (l : loc) (R : iProp) : iProp :=
( N γ, heapN N heap_ctx heapN inv N (lock_inv γ l R))%I. ( N γ, heapN N heap_ctx inv N (lock_inv γ l R))%I.
Definition locked (l : loc) (R : iProp) : iProp := Definition locked (l : loc) (R : iProp) : iProp :=
( N γ, heapN N heap_ctx heapN ( N γ, heapN N heap_ctx
inv N (lock_inv γ l R) own γ (Excl ()))%I. inv N (lock_inv γ l R) own γ (Excl ()))%I.
Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l). Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
...@@ -48,7 +47,7 @@ Proof. rewrite /is_lock. iDestruct 1 as (N γ) "(?&?&?&_)"; eauto. Qed. ...@@ -48,7 +47,7 @@ Proof. rewrite /is_lock. iDestruct 1 as (N γ) "(?&?&?&_)"; eauto. Qed.
Lemma newlock_spec N (R : iProp) Φ : Lemma newlock_spec N (R : iProp) Φ :
heapN N heapN N
heap_ctx heapN R ( l, is_lock l R - Φ #l) WP newlock #() {{ Φ }}. heap_ctx R ( l, is_lock l R - Φ #l) WP newlock #() {{ Φ }}.
Proof. Proof.
iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock. iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. wp_alloc l as "Hl". wp_seq. wp_alloc l as "Hl".
......
...@@ -12,13 +12,12 @@ Notation "e1 || e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope. ...@@ -12,13 +12,12 @@ Notation "e1 || e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
Global Opaque par. Global Opaque par.
Section proof. Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}. Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ). Local Notation iProp := (iPropG heap_lang Σ).
Lemma par_spec (Ψ1 Ψ2 : val iProp) e (f1 f2 : val) (Φ : val iProp) : Lemma par_spec (Ψ1 Ψ2 : val iProp) e (f1 f2 : val) (Φ : val iProp) :
heapN N to_val e = Some (f1,f2)%V heapN N to_val e = Some (f1,f2)%V
(heap_ctx heapN WP f1 #() {{ Ψ1 }} WP f2 #() {{ Ψ2 }} (heap_ctx WP f1 #() {{ Ψ1 }} WP f2 #() {{ Ψ2 }}
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
WP par e {{ Φ }}. WP par e {{ Φ }}.
Proof. Proof.
...@@ -34,7 +33,7 @@ Qed. ...@@ -34,7 +33,7 @@ Qed.
Lemma wp_par (Ψ1 Ψ2 : val iProp) Lemma wp_par (Ψ1 Ψ2 : val iProp)
(e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val iProp) : (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val iProp) :
heapN N heapN N
(heap_ctx heapN WP e1 {{ Ψ1 }} WP e2 {{ Ψ2 }} (heap_ctx WP e1 {{ Ψ1 }} WP e2 {{ Ψ2 }}
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
WP e1 || e2 {{ Φ }}. WP e1 || e2 {{ Φ }}.
Proof. Proof.
......
...@@ -28,8 +28,7 @@ Proof. destruct H as (?&?). split. apply: inGF_inG. Qed. ...@@ -28,8 +28,7 @@ Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
(** Now we come to the Iris part of the proof. *) (** Now we come to the Iris part of the proof. *)
Section proof. Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}. Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ). Local Notation iProp := (iPropG heap_lang Σ).
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val iProp) : iProp := Definition spawn_inv (γ : gname) (l : loc) (Ψ : val iProp) : iProp :=
...@@ -37,7 +36,7 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp := ...@@ -37,7 +36,7 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp :=
v, lv = SOMEV v (Ψ v own γ (Excl ()))))%I. v, lv = SOMEV v (Ψ v own γ (Excl ()))))%I.
Definition join_handle (l : loc) (Ψ : val iProp) : iProp := Definition join_handle (l : loc) (Ψ : val iProp) : iProp :=
(heapN N γ, heap_ctx heapN own γ (Excl ()) (heapN N γ, heap_ctx own γ (Excl ())
inv N (spawn_inv γ l Ψ))%I. inv N (spawn_inv γ l Ψ))%I.
Typeclasses Opaque join_handle. Typeclasses Opaque join_handle.
...@@ -53,7 +52,7 @@ Proof. solve_proper. Qed. ...@@ -53,7 +52,7 @@ Proof. solve_proper. Qed.
Lemma spawn_spec (Ψ : val iProp) e (f : val) (Φ : val iProp) : Lemma spawn_spec (Ψ : val iProp) e (f : val) (Φ : val iProp) :
to_val e = Some f to_val e = Some f
heapN N heapN N
heap_ctx heapN WP f #() {{ Ψ }} ( l, join_handle l Ψ - Φ #l) heap_ctx WP f #() {{ Ψ }} ( l, join_handle l Ψ - Φ #l)
WP spawn e {{ Φ }}. WP spawn e {{ Φ }}.
Proof. Proof.
iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn. iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn.
......
...@@ -6,8 +6,7 @@ Import uPred. ...@@ -6,8 +6,7 @@ Import uPred.
Ltac wp_strip_later ::= iNext. Ltac wp_strip_later ::= iNext.
Section heap. Section heap.
Context {Σ : gFunctors} `{heapG Σ}. Context `{heapG Σ}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG heap_lang Σ. Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val iPropG heap_lang Σ. Implicit Types Φ : val iPropG heap_lang Σ.
Implicit Types Δ : envs (iResUR heap_lang (globalF Σ)). Implicit Types Δ : envs (iResUR heap_lang (globalF Σ)).
...@@ -16,9 +15,9 @@ Global Instance into_sep_mapsto l q v : ...@@ -16,9 +15,9 @@ Global Instance into_sep_mapsto l q v :
IntoSep false (l {q} v) (l {q/2} v) (l {q/2} v). IntoSep false (l {q} v) (l {q/2} v) (l {q/2} v).
Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed. Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed.
Lemma tac_wp_alloc Δ Δ' N E j e v Φ : Lemma tac_wp_alloc Δ Δ' E j e v Φ :
to_val e = Some v to_val e = Some v
(Δ heap_ctx N) nclose N E (Δ heap_ctx) nclose heapN E
IntoLaterEnvs Δ Δ' IntoLaterEnvs Δ Δ'
( l, Δ'', ( l, Δ'',
envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ'' envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ''
...@@ -32,8 +31,8 @@ Proof. ...@@ -32,8 +31,8 @@ Proof.
by rewrite right_id HΔ'. by rewrite right_id HΔ'.
Qed. Qed.
Lemma tac_wp_load Δ Δ' N E i l q v Φ : Lemma tac_wp_load Δ Δ' E i l q v Φ :
(Δ heap_ctx N) nclose N E (Δ heap_ctx) nclose heapN E
IntoLaterEnvs Δ Δ' IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I envs_lookup i Δ' = Some (false, l {q} v)%I
(Δ' |={E}=> Φ v) (Δ' |={E}=> Φ v)
...@@ -44,9 +43,9 @@ Proof. ...@@ -44,9 +43,9 @@ Proof.
by apply later_mono, sep_mono_r, wand_mono. by apply later_mono, sep_mono_r, wand_mono.
Qed. Qed.
Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ : Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
to_val e = Some v' to_val e = Some v'
(Δ heap_ctx N) nclose N E (Δ heap_ctx) nclose heapN E
IntoLaterEnvs Δ Δ' IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ'' envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
...@@ -58,9 +57,9 @@ Proof. ...@@ -58,9 +57,9 @@ Proof.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono. rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed. Qed.
Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ : Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
(Δ heap_ctx N) nclose N E (Δ heap_ctx) nclose heapN E
IntoLaterEnvs Δ Δ' IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I v v1 envs_lookup i Δ' = Some (false, l {q} v)%I v v1
(Δ' |={E}=> Φ (LitV (LitBool false))) (Δ' |={E}=> Φ (LitV (LitBool false)))
...@@ -71,9 +70,9 @@ Proof. ...@@ -71,9 +70,9 @@ Proof.
by apply later_mono, sep_mono_r, wand_mono. by apply later_mono, sep_mono_r, wand_mono.
Qed. Qed.
Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l v e1 v1 e2 v2 Φ : Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
(Δ heap_ctx N) nclose N E (Δ heap_ctx) nclose heapN E
IntoLaterEnvs Δ Δ' IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I v = v1 envs_lookup i Δ' = Some (false, l v)%I v = v1
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ'' envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
...@@ -101,7 +100,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) := ...@@ -101,7 +100,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
[reshape_expr e ltac:(fun K e' => [reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with Alloc _ => wp_bind K end) match eval hnf in e' with Alloc _ => wp_bind K end)
|fail 1 "wp_alloc: cannot find 'Alloc' in" e]; |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
eapply tac_wp_alloc with _ _ H _; eapply tac_wp_alloc with _ H _;
[let e' := match goal with |- to_val ?e' = _ => e' end in [let e' := match goal with |- to_val ?e' = _ => e' end in
wp_done || fail "wp_alloc:" e' "not a value" wp_done || fail "wp_alloc:" e' "not a value"
|iAssumption || fail "wp_alloc: cannot find heap_ctx" |iAssumption || fail "wp_alloc: cannot find heap_ctx"
......
...@@ -14,7 +14,7 @@ Definition client : expr := ...@@ -14,7 +14,7 @@ Definition client : expr :=
Global Opaque worker client. Global Opaque worker client.
Section client. Section client.
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace). Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (N : namespace).
Local Notation iProp := (iPropG heap_lang Σ). Local Notation iProp := (iPropG heap_lang Σ).
Definition y_inv (q : Qp) (l : loc) : iProp := Definition y_inv (q : Qp) (l : loc) : iProp :=
...@@ -27,8 +27,7 @@ Section client. ...@@ -27,8 +27,7 @@ Section client.
Qed. Qed.
Lemma worker_safe q (n : Z) (b y : loc) : Lemma worker_safe q (n : Z) (b y : loc) :
heap_ctx heapN recv heapN N b (y_inv q y) heap_ctx recv N b (y_inv q y) WP worker n #b #y {{ _, True }}.
WP worker n #b #y {{ _, True }}.
Proof. Proof.
iIntros "[#Hh Hrecv]". wp_lam. wp_let. iIntros "[#Hh Hrecv]". wp_lam. wp_let.
wp_apply wait_spec; iFrame "Hrecv". wp_apply wait_spec; iFrame "Hrecv".
...@@ -37,12 +36,12 @@ Section client. ...@@ -37,12 +36,12 @@ Section client.
iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros (v) "_"]. iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros (v) "_"].
Qed. Qed.
Lemma client_safe : heapN N heap_ctx heapN WP client {{ _, True }}. Lemma client_safe : heapN N heap_ctx WP client {{ _, True }}.
Proof. Proof.
iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let. iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
wp_apply (newbarrier_spec heapN N (y_inv 1 y)); first done. wp_apply (newbarrier_spec N (y_inv 1 y)); first done.
iFrame "Hh". iIntros (l) "[Hr Hs]". wp_let. iFrame "Hh". iIntros (l) "[Hr Hs]". wp_let.
iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); first done. iApply (wp_par N (λ _, True%I) (λ _, True%I)); first done.
iFrame "Hh". iSplitL "Hy Hs". iFrame "Hh". iSplitL "Hy Hs".
- (* The original thread, the sender. *) - (* The original thread, the sender. *)
wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done]. wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
...@@ -52,7 +51,7 @@ Section client. ...@@ -52,7 +51,7 @@ Section client.
iDestruct (recv_weaken with "[] Hr") as "Hr". iDestruct (recv_weaken with "[] Hr") as "Hr".
{ iIntros "Hy". by iApply (y_inv_split with "Hy"). } { iIntros "Hy". by iApply (y_inv_split with "Hy"). }
iPvs (recv_split with "Hr") as "[H1 H2]"; first done. iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); eauto. iApply (wp_par N (λ _, True%I) (λ _, True%I)); eauto.
iFrame "Hh"; iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ >"]]; iFrame "Hh"; iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ >"]];
iApply worker_safe; by iSplit. iApply worker_safe; by iSplit.
Qed. Qed.
...@@ -65,8 +64,8 @@ Section ClosedProofs. ...@@ -65,8 +64,8 @@ Section ClosedProofs.
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{