Commit be558596 authored by Ralf Jung's avatar Ralf Jung

strengthen parallel composition: it strips away a later

parent 3f61f05d
Pipeline #265 passed with stage
...@@ -53,7 +53,8 @@ Section client. ...@@ -53,7 +53,8 @@ Section client.
wp_let. (ewp eapply (wp_par heapN N (λ _, True%I) (λ _, True%I))); eauto. wp_let. (ewp eapply (wp_par heapN N (λ _, True%I) (λ _, True%I))); eauto.
rewrite 2!{1}[heap_ctx _]always_sep_dup !assoc [(_ heap_ctx _)%I]comm. rewrite 2!{1}[heap_ctx _]always_sep_dup !assoc [(_ heap_ctx _)%I]comm.
ecancel [heap_ctx _]. sep_split right: []; last first. ecancel [heap_ctx _]. sep_split right: []; last first.
{ do 2 apply forall_intro=>_. apply wand_intro_l. eauto with I. } { do 2 apply forall_intro=>_. apply wand_intro_l.
eauto using later_intro with I. }
sep_split left: [send heapN _ _ _; heap_ctx _; y _]%I. sep_split left: [send heapN _ _ _; heap_ctx _; y _]%I.
- (* The original thread, the sender. *) - (* The original thread, the sender. *)
(ewp eapply wp_store); eauto with I. strip_later. (ewp eapply wp_store); eauto with I. strip_later.
...@@ -68,7 +69,8 @@ Section client. ...@@ -68,7 +69,8 @@ Section client.
(ewp eapply (wp_par heapN N (λ _, True%I) (λ _, True%I))); eauto. (ewp eapply (wp_par heapN N (λ _, True%I) (λ _, True%I))); eauto.
do 2 rewrite {1}[heap_ctx _]always_sep_dup. do 2 rewrite {1}[heap_ctx _]always_sep_dup.
ecancel [heap_ctx _]. rewrite !assoc. sep_split right: []; last first. ecancel [heap_ctx _]. rewrite !assoc. sep_split right: []; last first.
{ do 2 apply forall_intro=>_. apply wand_intro_l. eauto with I. } { do 2 apply forall_intro=>_. apply wand_intro_l.
eauto using later_intro with I. }
sep_split left: [recv heapN _ _ _; heap_ctx _]%I; by rewrite -worker_safe comm. sep_split left: [recv heapN _ _ _; heap_ctx _]%I; by rewrite -worker_safe comm.
Qed. Qed.
End client. End client.
......
...@@ -22,7 +22,7 @@ Local Notation iProp := (iPropG heap_lang Σ). ...@@ -22,7 +22,7 @@ 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 #> f1 #() {{ Ψ1 }} #> f2 #() {{ Ψ2 }} (heap_ctx heapN #> f1 #() {{ Ψ1 }} #> f2 #() {{ Ψ2 }}
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
#> par e {{ Φ }}. #> par e {{ Φ }}.
Proof. Proof.
intros. rewrite /par. intros. rewrite /par.
...@@ -35,16 +35,15 @@ Proof. ...@@ -35,16 +35,15 @@ Proof.
wp_proj; eauto using to_of_val. wp_proj; eauto using to_of_val.
wp_focus (f2 _). rewrite wp_frame_r wp_frame_l. apply wp_mono=>v2. wp_let. wp_focus (f2 _). rewrite wp_frame_r wp_frame_l. apply wp_mono=>v2. wp_let.
ewp eapply join_spec; eauto using to_of_val. apply sep_mono_r. ewp eapply join_spec; eauto using to_of_val. apply sep_mono_r.
apply forall_intro=>v1. apply wand_intro_l. wp_let. apply forall_intro=>v1. apply wand_intro_l.
etransitivity; last by (eapply wp_value, to_val_Pair; eapply to_of_val). rewrite (forall_elim v1) (forall_elim v2). rewrite assoc wand_elim_r.
rewrite (forall_elim v1) (forall_elim v2). rewrite assoc. wp_let. eapply wp_value, to_val_Pair; eapply to_of_val.
eapply wand_apply_r'; done.
Qed. Qed.
Lemma wp_par (Ψ1 Ψ2 : val iProp) (e1 e2 : expr []) (Φ : val iProp) : Lemma wp_par (Ψ1 Ψ2 : val iProp) (e1 e2 : expr []) (Φ : val iProp) :
heapN N heapN N
(heap_ctx heapN #> e1 {{ Ψ1 }} #> e2 {{ Ψ2 }} (heap_ctx heapN #> e1 {{ Ψ1 }} #> e2 {{ Ψ2 }}
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
#> ParV e1 e2 {{ Φ }}. #> ParV e1 e2 {{ Φ }}.
Proof. Proof.
intros. rewrite -par_spec //. apply sep_mono_r. intros. rewrite -par_spec //. apply sep_mono_r.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment