Commit 00444b07 authored by Ralf Jung's avatar Ralf Jung

new definition of atomicity: reduces in one step to sth. that doesn't reduce further

parent 9d2e164b
......@@ -53,8 +53,7 @@ Proof.
iIntros (Φ) "HP HΦ".
iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
subst v2. iSplit. iApply "HΦ"; by iSplit. by iApply big_sepL_nil.
iSplitL; last by iApply big_sepL_nil. iApply "HΦ". by iSplit.
Qed.
Lemma wp_load_pst E σ l v :
......
......@@ -187,6 +187,7 @@ Lemma atomic_correct e : atomic e → language.atomic (to_expr e).
Proof.
intros He. apply ectx_language_atomic.
- intros σ e' σ' ef.
intros H; apply language.val_irreducible; revert H.
destruct e; simpl; try done; repeat (case_match; try done);
inversion 1; rewrite ?to_of_val; eauto. subst.
unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
......
......@@ -90,7 +90,7 @@ Section ectx_language.
Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed.
Lemma ectx_language_atomic e :
( σ e' σ' efs, head_step e σ e' σ' efs is_Some (to_val e'))
( σ e' σ' efs, head_step e σ e' σ' efs irreducible e' σ')
( K e', e = fill K e' to_val e' = None K = empty_ectx)
atomic e.
Proof.
......
......@@ -39,19 +39,17 @@ Proof.
Qed.
Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
atomic e1
head_reducible e1 σ1
ownP σ1 ( v2 σ2 efs,
head_step e1 σ1 (of_val v2) σ2 efs ownP σ2 -
Φ v2 [ list] ef efs, WP ef {{ _, True }})
ownP σ1 ( e2 σ2 efs,
head_step e1 σ1 e2 σ2 efs ownP σ2 -
default False (to_val e2) Φ [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}.
Proof.
iIntros (??) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
iIntros (?) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
iIntros (???) "[% ?]". iApply "H". eauto.
Qed.
Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
atomic e1
head_reducible e1 σ1
( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs'
σ2 = σ2' to_val e2' = Some v2 efs = efs')
......@@ -61,7 +59,6 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
Proof. eauto using wp_lift_atomic_det_step. Qed.
Lemma wp_lift_atomic_det_head_step' {E e1} σ1 v2 σ2 :
atomic e1
head_reducible e1 σ1
( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs'
σ2 = σ2' to_val e2' = Some v2 [] = efs')
......
......@@ -34,8 +34,10 @@ Section language.
Definition reducible (e : expr Λ) (σ : state Λ) :=
e' σ' efs, prim_step e σ e' σ' efs.
Definition irreducible (e : expr Λ) (σ : state Λ) :=
e' σ' efs, ~prim_step e σ e' σ' efs.
Definition atomic (e : expr Λ) : Prop :=
σ e' σ' efs, prim_step e σ e' σ' efs is_Some (to_val e').
σ e' σ' efs, prim_step e σ e' σ' efs irreducible e' σ'.
Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
| step_atomic e1 σ1 e2 σ2 efs t1 t2 :
ρ1 = (t1 ++ e1 :: t2, σ1)
......@@ -47,6 +49,8 @@ Section language.
Proof. intros <-. by rewrite to_of_val. Qed.
Lemma reducible_not_val e σ : reducible e σ to_val e = None.
Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
Lemma val_irreducible e σ : is_Some (to_val e) irreducible e σ.
Proof. intros [??] ??? ?%val_stuck. by destruct (to_val e). Qed.
Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
End language.
......
......@@ -45,23 +45,21 @@ Qed.
(** Derived lifting lemmas. *)
Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
atomic e1
reducible e1 σ1
( ownP σ1 v2 σ2 efs, prim_step e1 σ1 (of_val v2) σ2 efs ownP σ2 -
Φ v2 [ list] ef efs, WP ef {{ _, True }})
( ownP σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ownP σ2 -
default False (to_val e2) Φ [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}.
Proof.
iIntros (Hatomic ?) "[Hσ H]". iApply (wp_lift_step E _ e1).
iIntros (?) "[Hσ H]". iApply (wp_lift_step E _ e1).
iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver. iModIntro.
iExists σ1. iFrame "Hσ"; iSplit; eauto.
iNext; iIntros (e2 σ2 efs) "[% Hσ]".
edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
iDestruct ("H" $! v2 σ2 efs with "[Hσ]") as "[HΦ $]"; first by eauto.
iMod "Hclose". iApply wp_value; auto using to_of_val.
iDestruct ("H" $! e2 σ2 efs with "[Hσ]") as "[HΦ $]"; first by eauto.
destruct (to_val e2) eqn:?; last by iExFalso.
iMod "Hclose". iApply wp_value; auto using to_of_val. done.
Qed.
Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
atomic e1
reducible e1 σ1
( e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs'
σ2 = σ2' to_val e2' = Some v2 efs = efs')
......@@ -69,9 +67,9 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
Φ v2 [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}.
Proof.
iIntros (?? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
iFrame. iNext. iIntros (v2' σ2' efs') "[% Hσ2']".
edestruct Hdet as (->&->%of_to_val%(inj of_val)&->). done. by iApply "Hσ2".
iIntros (? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
iFrame. iNext. iIntros (e2' σ2' efs') "[% Hσ2']".
edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2".
Qed.
Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
......
......@@ -197,9 +197,14 @@ Proof.
{ iDestruct "H" as (v') "[% ?]"; simplify_eq. }
iMod ("H" $! σ1 with "Hσ") as "[$ H]".
iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
iMod ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
iMod ("H" with "* []") as "(Hphy & H & $)"; first done.
rewrite wp_unfold /wp_pre. iDestruct "H" as "[H|H]".
- iDestruct "H" as (v) "[% >>?]". iModIntro. iFrame.
rewrite -(of_to_val e2 v) //. by iApply wp_value'.
- iDestruct "H" as "[_ H]".
iMod ("H" with "* Hphy") as "[H _]".
iDestruct "H" as %(? & ? & ? & ?). exfalso.
by eapply (Hatomic _ _ _ _ Hstep).
Qed.
Lemma wp_fupd_step E1 E2 e P Φ :
......
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