Commit e6aeb885 authored by Ralf Jung's avatar Ralf Jung

timing: make fewer things opaque

parent 71abda4d
Pipeline #3565 passed with stage
in 10 minutes and 29 seconds
...@@ -53,8 +53,6 @@ Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp Σ) : ...@@ -53,8 +53,6 @@ Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp Σ) :
PersistentP (barrier_ctx γ l P). PersistentP (barrier_ctx γ l P).
Proof. apply _. Qed. Proof. apply _. Qed.
Typeclasses Opaque barrier_ctx send recv.
(** Setoids *) (** Setoids *)
Global Instance ress_ne n : Proper (dist n ==> (=) ==> dist n) ress. Global Instance ress_ne n : Proper (dist n ==> (=) ==> dist n) ress.
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
...@@ -103,7 +101,7 @@ Proof. ...@@ -103,7 +101,7 @@ Proof.
{ iNext. rewrite /barrier_inv /=. iFrame. { iNext. rewrite /barrier_inv /=. iFrame.
iExists (const P). rewrite !big_sepS_singleton /=. eauto. } iExists (const P). rewrite !big_sepS_singleton /=. eauto. }
iAssert (barrier_ctx γ' l P)%I as "#?". iAssert (barrier_ctx γ' l P)%I as "#?".
{ rewrite /barrier_ctx. by repeat iSplit. } { done. }
iAssert (sts_ownS γ' (i_states γ) {[Change γ]} iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
sts_ownS γ' low_states {[Send]})%I with ">[-]" as "[Hr Hs]". sts_ownS γ' low_states {[Send]})%I with ">[-]" as "[Hr Hs]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed. { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
...@@ -111,15 +109,15 @@ Proof. ...@@ -111,15 +109,15 @@ Proof.
- iApply (sts_own_weaken with "Hγ'"); - iApply (sts_own_weaken with "Hγ'");
auto using sts.closed_op, i_states_closed, low_states_closed; auto using sts.closed_op, i_states_closed, low_states_closed;
abstract set_solver. } abstract set_solver. }
iModIntro. rewrite /recv /send. iSplitL "Hr". iModIntro. iSplitL "Hr".
- iExists γ', P, P, γ. iFrame. auto. - iExists γ', P, P, γ. iFrame. auto.
- auto. - rewrite /send. auto.
Qed. Qed.
Lemma signal_spec l P : Lemma signal_spec l P :
{{{ send l P P }}} signal #l {{{ RET #(); True }}}. {{{ send l P P }}} signal #l {{{ RET #(); True }}}.
Proof. Proof.
rewrite /signal /send /barrier_ctx /=. rewrite /signal /=.
iIntros (Φ) "[Hs HP] HΦ". iDestruct "Hs" as (γ) "[#Hsts Hγ]". wp_let. iIntros (Φ) "[Hs HP] HΦ". iDestruct "Hs" as (γ) "[#Hsts Hγ]". wp_let.
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]") iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto. as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
...@@ -127,7 +125,7 @@ Proof. ...@@ -127,7 +125,7 @@ Proof.
iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ". iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ".
iMod ("Hclose" $! (State High I) ( : set token) with "[-]"); last done. iMod ("Hclose" $! (State High I) ( : set token) with "[-]"); last done.
iSplit; [iPureIntro; by eauto using signal_step|]. iSplit; [iPureIntro; by eauto using signal_step|].
rewrite {2}/barrier_inv /ress /=. iNext. iFrame "Hl". rewrite /barrier_inv /ress /=. iNext. iFrame "Hl".
iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp". iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
iNext. iIntros "_"; by iApply "Hr". iNext. iIntros "_"; by iApply "Hr".
Qed. Qed.
...@@ -135,14 +133,14 @@ Qed. ...@@ -135,14 +133,14 @@ Qed.
Lemma wait_spec l P: Lemma wait_spec l P:
{{{ recv l P }}} wait #l {{{ RET #(); P }}}. {{{ recv l P }}} wait #l {{{ RET #(); P }}}.
Proof. Proof.
rename P into R; rewrite /recv /barrier_ctx. rename P into R.
iIntros (Φ) "Hr HΦ"; iDestruct "Hr" as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)". iIntros (Φ) "Hr HΦ"; iDestruct "Hr" as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
iLöb as "IH". wp_rec. wp_bind (! _)%E. iLöb as "IH". wp_rec. wp_bind (! _)%E.
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]") iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto. as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
wp_load. destruct p. wp_load. destruct p.
- iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ". - iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
{ iSplit; first done. rewrite {2}/barrier_inv /=. by iFrame. } { iSplit; first done. rewrite /barrier_inv /=. by iFrame. }
iAssert (sts_ownS γ (i_states i) {[Change i]})%I with ">[Hγ]" as "Hγ". iAssert (sts_ownS γ (i_states i) {[Change i]})%I with ">[Hγ]" as "Hγ".
{ iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. } { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
iModIntro. wp_if. iModIntro. wp_if.
...@@ -155,7 +153,7 @@ Proof. ...@@ -155,7 +153,7 @@ Proof.
{ iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". } { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
iMod ("Hclose" $! (State High (I {[ i ]})) ( : set token) with "[HΨ' Hl Hsp]"). iMod ("Hclose" $! (State High (I {[ i ]})) ( : set token) with "[HΨ' Hl Hsp]").
{ iSplit; [iPureIntro; by eauto using wait_step|]. { iSplit; [iPureIntro; by eauto using wait_step|].
rewrite {2}/barrier_inv /=. iNext. iFrame "Hl". iExists Ψ; iFrame. auto. } rewrite /barrier_inv /=. iNext. iFrame "Hl". iExists Ψ; iFrame. auto. }
iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto. iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
iModIntro. wp_if. iModIntro. wp_if.
iApply "HΦ". iApply "HQR". by iRewrite "Heq". iApply "HΦ". iApply "HQR". by iRewrite "Heq".
...@@ -164,7 +162,7 @@ Qed. ...@@ -164,7 +162,7 @@ Qed.
Lemma recv_split E l P1 P2 : Lemma recv_split E l P1 P2 :
N E recv l (P1 P2) ={E}= recv l P1 recv l P2. N E recv l (P1 P2) ={E}= recv l P1 recv l P2.
Proof. Proof.
rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx. rename P1 into R1; rename P2 into R2.
iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)". iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]") iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto. as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
...@@ -175,7 +173,7 @@ Proof. ...@@ -175,7 +173,7 @@ Proof.
iMod ("Hclose" $! (State p ({[i1; i2]} I {[i]})) iMod ("Hclose" $! (State p ({[i1; i2]} I {[i]}))
{[Change i1; Change i2 ]} with "[-]") as "Hγ". {[Change i1; Change i2 ]} with "[-]") as "Hγ".
{ iSplit; first by eauto using split_step. { iSplit; first by eauto using split_step.
rewrite {2}/barrier_inv /=. iNext. iFrame "Hl". rewrite /barrier_inv /=. iNext. iFrame "Hl".
by iApply (ress_split with "HQ Hi1 Hi2 HQR"). } by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }
iAssert (sts_ownS γ (i_states i1) {[Change i1]} iAssert (sts_ownS γ (i_states i1) {[Change i1]}
sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]". sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]".
...@@ -184,14 +182,14 @@ Proof. ...@@ -184,14 +182,14 @@ Proof.
- iApply (sts_own_weaken with "Hγ"); - iApply (sts_own_weaken with "Hγ");
eauto using sts.closed_op, i_states_closed. eauto using sts.closed_op, i_states_closed.
abstract set_solver. } abstract set_solver. }
iModIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx. iModIntro; iSplitL "Hγ1".
- iExists γ, P, R1, i1. iFrame; auto. - iExists γ, P, R1, i1. iFrame; auto.
- iExists γ, P, R2, i2. iFrame; auto. - iExists γ, P, R2, i2. iFrame; auto.
Qed. Qed.
Lemma recv_weaken l P1 P2 : (P1 - P2) - recv l P1 - recv l P2. Lemma recv_weaken l P1 P2 : (P1 - P2) - recv l P1 - recv l P2.
Proof. Proof.
rewrite /recv. iIntros "HP". iDestruct 1 as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)". iIntros "HP". iDestruct 1 as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
iExists γ, P, Q, i. iFrame "Hctx Hγ Hi". iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
iNext. iIntros "HQ". by iApply "HP"; iApply "HP1". iNext. iIntros "HQ". by iApply "HP"; iApply "HP1".
Qed. Qed.
......
...@@ -36,8 +36,6 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ : ...@@ -36,8 +36,6 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :
Definition join_handle (l : loc) (Ψ : val iProp Σ) : iProp Σ := Definition join_handle (l : loc) (Ψ : val iProp Σ) : iProp Σ :=
( γ, own γ (Excl ()) inv N (spawn_inv γ l Ψ))%I. ( γ, own γ (Excl ()) inv N (spawn_inv γ l Ψ))%I.
Typeclasses Opaque join_handle.
Global Instance spawn_inv_ne n γ l : Global Instance spawn_inv_ne n γ l :
Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γ l). Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γ l).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
...@@ -65,7 +63,7 @@ Qed. ...@@ -65,7 +63,7 @@ Qed.
Lemma join_spec (Ψ : val iProp Σ) l : Lemma join_spec (Ψ : val iProp Σ) l :
{{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}. {{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
Proof. Proof.
rewrite /join_handle; iIntros (Φ) "H HΦ". iDestruct "H" as (γ) "[Hγ #?]". iIntros (Φ) "H HΦ". iDestruct "H" as (γ) "[Hγ #?]".
iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose". iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst. wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|]. - iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
......
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