Commit 90da10c1 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

WIP: Change awp in an attempt to get a stronger bind rule.

parent ec7fc927
...@@ -24,7 +24,7 @@ Definition a_run : val := λ: "x", ...@@ -24,7 +24,7 @@ Definition a_run : val := λ: "x",
Definition a_atomic : val := λ: "x" "env" "l", Definition a_atomic : val := λ: "x" "env" "l",
acquire "l";; acquire "l";;
let: "k" := newlock #() in let: "k" := newlock #() in
let: "a" := "x" "env" "k" in let: "a" := "x" #() "env" "k" in
release "l";; release "l";;
"a". "a".
...@@ -42,11 +42,11 @@ Definition a_par : val := λ: "x" "y" "env" "l", ...@@ -42,11 +42,11 @@ Definition a_par : val := λ: "x" "y" "env" "l",
Definition amonadN := nroot .@ "amonad". Definition amonadN := nroot .@ "amonad".
Section a_wp. Section a_wp.
Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapG Σ}. Context `{heapG Σ, flockG Σ, locking_heapG Σ}.
(* X ⊆ σ^{-1}(L) *) (* X ⊆ σ^{-1}(L) *)
Definition correct_locks (X : gset val) (preσ : gset loc) : Prop := Definition correct_locks (X : gset val) (preσ : gset loc) : Prop :=
set_Forall (fun x => l : loc, x = #l l preσ) X. set_Forall (λ v, l : loc, v = #l l preσ) X.
Definition env_inv (env : val) : iProp Σ := Definition env_inv (env : val) : iProp Σ :=
( (X : gset val) (σ : gmap loc level), ( (X : gset val) (σ : gmap loc level),
...@@ -57,48 +57,51 @@ Section a_wp. ...@@ -57,48 +57,51 @@ Section a_wp.
Definition awp (e : expr) Definition awp (e : expr)
(R : iProp Σ) (Φ : val iProp Σ) : iProp Σ := (R : iProp Σ) (Φ : val iProp Σ) : iProp Σ :=
( (γ : flock_name) (π : frac) (env : val) (l : val), WP e {{ ev, (γ : flock_name) (π : frac) (env : val) (l : val),
is_flock amonadN γ l (env_inv env R) - is_flock amonadN γ l (env_inv env R) -
unflocked γ π - unflocked γ π -
WP e env l {{ v, WP ev env l {{ v, Φ v unflocked γ π }}
Φ v unflocked γ π }} }}%I.
)%I. End a_wp.
Section a_wp_rules.
Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapG Σ}.
Lemma awp_ret e R Φ : Lemma awp_ret e R Φ :
WP e {{ Φ }} - awp (a_ret e) R Φ. WP e {{ Φ }} - awp (a_ret e) R Φ.
Proof. Proof.
iIntros "Hwp" (γ π env l) "#Hlock Hunfl". iIntros "Hwp". rewrite /awp /a_ret. wp_apply (wp_wand with "Hwp").
rewrite /a_ret. wp_bind e. iIntros (v) "HΦ". wp_lam.
iApply (wp_wand with "Hwp"); iIntros (v) "HΦ /=". iIntros (γ π env l) "#Hlock Hunfl". do 2 wp_lam. iFrame.
do 3 wp_lam. iFrame.
Qed. Qed.
(* Use [IntoVal] everywhere *) (* Use [IntoVal] everywhere *)
Lemma awp_bind (fe ve : expr) (f v : val) R Φ : Lemma awp_bind (f e : expr) fv R Φ :
IntoVal fe f IntoVal f fv
IntoVal ve v awp e R (λ ev, awp (fv ev) R Φ) -
awp ve R (λ w, awp (fe w) R Φ) - awp (a_bind fe ve) R Φ. awp (a_bind f e) R Φ.
Proof. Proof.
iIntros (? ?) "Hwp". iIntros (γ π env l) "#Hlock Hunfl". iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_bind. wp_lam. wp_bind e.
rewrite -(of_to_val fe f); last done. iApply (wp_wand with "Hwp"). iIntros (ev) "Hwp". wp_lam.
rewrite -(of_to_val ve v); last done. iIntros (γ π env l) "#Hlock Hunfl". do 2 wp_lam. wp_bind (ev env l).
rewrite /a_bind /=. do 4 wp_lam.
wp_bind (v env l).
iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp". iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
iIntros (w) "[Hwp Hunfl]". wp_let. by iApply "Hwp". iIntros (w) "[Hwp Hunfl]". wp_let. wp_apply (wp_wand with "Hwp").
iIntros (v) "H". by iApply ("H" with "[$]").
Qed. Qed.
Lemma awp_atomic (v : val) R Φ `{Timeless _ R} : Lemma awp_atomic e (ev : val) R Φ `{Timeless _ R} :
(R - R', Timeless R' R' awp v R' (λ w, R' - R Φ w)) - IntoVal e ev
awp (a_atomic v) R Φ. (R - R', Timeless R' R' awp (ev #()) R' (λ w, R' - R Φ w)) -
awp (a_atomic e) R Φ.
Proof. Proof.
iIntros "Hwp" (γ π env l) "#Hlock1 Hunfl1". iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic. wp_lam.
rewrite /a_atomic /=. do 3 wp_let. iIntros (γ π env l) "#Hlock1 Hunfl1". do 2 wp_let.
wp_apply (acquire_cancel_spec with "[$]"). wp_apply (acquire_cancel_spec with "[$]").
iIntros "[Hflkd [Henv HR]] /=". wp_seq. iIntros "[Hflkd [Henv HR]] /=". wp_seq.
iDestruct ("Hwp" with "HR") as (R') "(% & HR' & Hwp)". iDestruct ("Hwp" with "HR") as (R') "(% & HR' & Hwp)".
wp_apply (newlock_cancel_spec amonadN (env_inv env R')%I with "[$Henv $HR']"). wp_apply (newlock_cancel_spec amonadN (env_inv env R')%I with "[$Henv $HR']").
iIntros (k γ') "[#Hlock2 Hunfl2]". wp_let. wp_bind (v env k). iIntros (k γ') "[#Hlock2 Hunfl2]". wp_let.
wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
iApply (wp_wand with "[Hwp Hunfl2]"); first by iApply "Hwp". iApply (wp_wand with "[Hwp Hunfl2]"); first by iApply "Hwp".
iIntros (w) "[HR Hunfl2]". wp_let. iIntros (w) "[HR Hunfl2]". wp_let.
iMod (cancel_lock with "Hlock2 Hunfl2") as "[Henv HR']". iMod (cancel_lock with "Hlock2 Hunfl2") as "[Henv HR']".
...@@ -107,15 +110,14 @@ Section a_wp. ...@@ -107,15 +110,14 @@ Section a_wp.
iIntros "Hunfl1". wp_seq. iFrame. iIntros "Hunfl1". wp_seq. iFrame.
Qed. Qed.
Lemma awp_atomic_env (ve : expr) (v : val) R Φ `{Timeless _ R} : Lemma awp_atomic_env e (ev : val) R Φ `{Timeless _ R} :
IntoVal ve v IntoVal e ev
( env, env_inv env - R - ( env, env_inv env - R -
WP ve env {{ w, env_inv env R Φ w }}) - WP ev env {{ w, env_inv env R Φ w }}) -
awp (a_atomic_env ve) R Φ. awp (a_atomic_env ev) R Φ.
Proof. Proof.
intros ?. rewrite -(of_to_val ve v); last done. iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env. wp_lam.
iIntros "Hwp" (γ π env l) "#Hlock Hunfl". iIntros (γ π env l) "#Hlock Hunfl". do 2 wp_lam.
rewrite /a_atomic_env /=. do 3 wp_lam.
wp_apply (acquire_cancel_spec with "[$]"). wp_apply (acquire_cancel_spec with "[$]").
iIntros "[Hflkd [Henv HR]] /=". wp_seq. iIntros "[Hflkd [Henv HR]] /=". wp_seq.
iDestruct ("Hwp" with "Henv HR") as "Hwp". iDestruct ("Hwp" with "Henv HR") as "Hwp".
...@@ -125,26 +127,28 @@ Section a_wp. ...@@ -125,26 +127,28 @@ Section a_wp.
iIntros "Hunfl". wp_seq. iFrame. iIntros "Hunfl". wp_seq. iFrame.
Qed. Qed.
Lemma awp_par (ve1 ve2 : expr) (v1 v2 : val) R (Ψ1 Ψ2 Φ : val iProp Σ) : Lemma awp_par e1 e2 (ev1 ev2 : val) R (Ψ1 Ψ2 Φ : val iProp Σ) :
IntoVal ve1 v1 IntoVal e1 ev1
IntoVal ve2 v2 IntoVal e2 ev2
awp ve1 R Ψ1 - awp ev1 R Ψ1 -
awp ve2 R Ψ2 - awp ev2 R Ψ2 -
( w1 w2, Ψ1 w1 - Ψ2 w2 - Φ (w1,w2)%V) - ( w1 w2, Ψ1 w1 - Ψ2 w2 - Φ (w1,w2)%V) -
awp (a_par ve1 ve2) R Φ. awp (a_par ev1 ev2) R Φ.
Proof. Proof.
intros ? ?. rewrite -(of_to_val ve1 v1); last done. rewrite -(of_to_val ve2 v2); last done. iIntros (<-%of_to_val <-%of_to_val) "Hwp1 Hwp2 HΦ".
iIntros "Hwp1 Hwp2 HΦ" (γ π env l) "#Hlock [Hunfl1 Hunfl2]". rewrite /awp /a_par. do 2 wp_lam.
rewrite /a_par /=. do 4 wp_lam. iIntros (γ π env l) "#Hlock [Hunfl1 Hunfl2]". do 2 wp_lam.
iApply (par_spec (λ v, Ψ1 v unflocked _ (π/2))%I iApply (par_spec (λ v, Ψ1 v unflocked _ (π/2))%I
(λ v, Ψ2 v unflocked _ (π/2))%I (λ v, Ψ2 v unflocked _ (π/2))%I
with "[Hwp1 Hunfl1] [Hwp2 Hunfl2]"). with "[Hwp1 Hunfl1] [Hwp2 Hunfl2]").
- wp_lam. by iApply "Hwp1". - wp_lam. wp_apply (wp_wand with "Hwp1").
- wp_lam. by iApply "Hwp2". iIntros (v) "Hwp1". by iApply "Hwp1".
- wp_lam. wp_apply (wp_wand with "Hwp2").
iIntros (v) "Hwp2". by iApply "Hwp2".
- iNext. iIntros (w1 w2) "[[HΨ1 $] [HΨ2 $]]". - iNext. iIntros (w1 w2) "[[HΨ1 $] [HΨ2 $]]".
iApply ("HΦ" with "[$] [$]"). iApply ("HΦ" with "[$] [$]").
Qed. Qed.
End a_wp. End a_wp_rules.
Section a_wp_run. Section a_wp_run.
Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapPreG Σ}. Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapPreG Σ}.
...@@ -160,13 +164,11 @@ Section a_wp_run. ...@@ -160,13 +164,11 @@ Section a_wp_run.
wp_apply (newlock_cancel_spec amonadN (env_inv env R)%I with "[Henv Hσ $HR]"). wp_apply (newlock_cancel_spec amonadN (env_inv env R)%I with "[Henv Hσ $HR]").
{ iExists , . iFrame. eauto. } { iExists , . iFrame. eauto. }
iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd. iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd.
iApply (wp_wand with "[Hwp Hunfl]"). wp_apply (wp_wand with "Hwp"). iIntros (v') "Hwp".
unfold awp. by iApply ("Hwp" with "Hlock"). iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
iIntros (w) "[HΦ Hunfl]". iIntros (w) "[HΦ Hunfl]". iApply "HΦ".
iApply "HΦ". by iMod (cancel_lock with "Hlock Hunfl") as "[HEnv HR]".
iMod (cancel_lock with "Hlock Hunfl") as "[HEnv HR]". done.
Qed. Qed.
End a_wp_run. End a_wp_run.
(* Definition locking_heapΣ : gFunctors := *) (* Definition locking_heapΣ : gFunctors := *)
......
...@@ -19,5 +19,4 @@ Section test. ...@@ -19,5 +19,4 @@ Section test.
iIntros "Hl". awp_pure _. iIntros "Hl". awp_pure _.
iApply (a_load_spec with "Hl"). iIntros "Hl". eauto. iApply (a_load_spec with "Hl"). iIntros "Hl". eauto.
Qed. Qed.
End test. End test.
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