Commit 24f054ec by Ralf Jung

### rename atomic_step -> atomic_acc

parent 1a004a76
Pipeline #9337 passed with stage
in 29 minutes and 5 seconds
 ... @@ -18,15 +18,16 @@ Section definition. ... @@ -18,15 +18,16 @@ Section definition. (Φ : A → B → PROP) (* post-condition *) (Φ : A → B → PROP) (* post-condition *) . . (** atomic_step as the "introduction form" of atomic updates *) (** atomic_acc as the "introduction form" of atomic updates: An accessor Definition atomic_step Eo Ei α P β Φ : PROP := that can be aborted back to [P]. *) Definition atomic_acc Eo Ei α P β Φ : PROP := (|={Eo, Ei}=> ∃ x, α x ∗ (|={Eo, Ei}=> ∃ x, α x ∗ ((α x ={Ei, Eo}=∗ P) ∧ (∀ y, β x y ={Ei, Eo}=∗ Φ x y)) ((α x ={Ei, Eo}=∗ P) ∧ (∀ y, β x y ={Ei, Eo}=∗ Φ x y)) )%I. )%I. Lemma atomic_step_wand Eo Ei α P1 P2 β Φ1 Φ2 : Lemma atomic_acc_wand Eo Ei α P1 P2 β Φ1 Φ2 : ((P1 -∗ P2) ∧ (∀ x y, Φ1 x y -∗ Φ2 x y)) -∗ ((P1 -∗ P2) ∧ (∀ x y, Φ1 x y -∗ Φ2 x y)) -∗ (atomic_step Eo Ei α P1 β Φ1 -∗ atomic_step Eo Ei α P2 β Φ2). (atomic_acc Eo Ei α P1 β Φ1 -∗ atomic_acc Eo Ei α P2 β Φ2). Proof. Proof. iIntros "HP12 AS". iMod "AS" as (x) "[Hα Hclose]". iIntros "HP12 AS". iMod "AS" as (x) "[Hα Hclose]". iModIntro. iExists x. iFrame "Hα". iSplit. iModIntro. iExists x. iFrame "Hα". iSplit. ... @@ -36,8 +37,8 @@ Section definition. ... @@ -36,8 +37,8 @@ Section definition. iApply "HP12". iApply "Hclose". done. iApply "HP12". iApply "Hclose". done. Qed. Qed. Lemma atomic_step_mask Eo Em α P β Φ : Lemma atomic_acc_mask Eo Em α P β Φ : atomic_step Eo (Eo∖Em) α P β Φ ⊣⊢ ∀ E, ⌜Eo ⊆ E⌝ → atomic_step E (E∖Em) α P β Φ. atomic_acc Eo (Eo∖Em) α P β Φ ⊣⊢ ∀ E, ⌜Eo ⊆ E⌝ → atomic_acc E (E∖Em) α P β Φ. Proof. Proof. iSplit; last first. iSplit; last first. { iIntros "Hstep". iApply ("Hstep" with "[% //]"). } { iIntros "Hstep". iApply ("Hstep" with "[% //]"). } ... @@ -50,21 +51,22 @@ Section definition. ... @@ -50,21 +51,22 @@ Section definition. - iIntros (y) "Hβ". iApply "Hclose'". iApply "Hclose". done. - iIntros (y) "Hβ". iApply "Hclose'". iApply "Hclose". done. Qed. Qed. (** atomic_update as a fixed-point of the equation (** atomic_update as a fixed-point of the equation AU = ∃ P. ▷ P ∗ □ (▷ P ==∗ α ∗ (α ==∗ AU) ∧ (β ==∗ Q)) AU = ∃ P. ▷ P ∗ □ (▷ P ==∗ α ∗ (α ==∗ AU) ∧ (β ==∗ Q)) *) = ∃ P. ▷ P ∗ □ (▷ P -∗ atomic_acc α AU β Q) *) Context Eo Em α β Φ. Context Eo Em α β Φ. Definition atomic_update_pre (Ψ : () → PROP) (_ : ()) : PROP := Definition atomic_update_pre (Ψ : () → PROP) (_ : ()) : PROP := (∃ (P : PROP), ▷ P ∗ (∃ (P : PROP), ▷ P ∗ □ (▷ P -∗ atomic_step Eo (Eo∖Em) α (Ψ ()) β Φ))%I. □ (▷ P -∗ atomic_acc Eo (Eo∖Em) α (Ψ ()) β Φ))%I. Local Instance atomic_update_pre_mono : BiMonoPred atomic_update_pre. Local Instance atomic_update_pre_mono : BiMonoPred atomic_update_pre. Proof. Proof. constructor. constructor. - iIntros (P1 P2) "#HP12". iIntros ([]) "AU". - iIntros (P1 P2) "#HP12". iIntros ([]) "AU". iDestruct "AU" as (P) "[HP #AS]". iExists P. iFrame. iDestruct "AU" as (P) "[HP #AS]". iExists P. iFrame. iIntros "!# HP". iApply (atomic_step_wand with "[HP12]"); last by iApply "AS". iIntros "!# HP". iApply (atomic_acc_wand with "[HP12]"); last by iApply "AS". iSplit; last by eauto. iApply "HP12". iSplit; last by eauto. iApply "HP12". - intros ??. solve_proper. - intros ??. solve_proper. Qed. Qed. ... @@ -87,14 +89,14 @@ Section lemmas. ... @@ -87,14 +89,14 @@ Section lemmas. Local Existing Instance atomic_update_pre_mono. Local Existing Instance atomic_update_pre_mono. Global Instance atomic_step_ne Eo Em n : Global Instance atomic_acc_ne Eo Em n : Proper ( Proper ( pointwise_relation A (dist n) ==> pointwise_relation A (dist n) ==> dist n ==> dist n ==> pointwise_relation A (pointwise_relation B (dist n)) ==> pointwise_relation A (pointwise_relation B (dist n)) ==> pointwise_relation A (pointwise_relation B (dist n)) ==> pointwise_relation A (pointwise_relation B (dist n)) ==> dist n dist n ) (atomic_step (PROP:=PROP) Eo Em). ) (atomic_acc (PROP:=PROP) Eo Em). Proof. solve_proper. Qed. Proof. solve_proper. Qed. Global Instance atomic_update_ne Eo Em n : Global Instance atomic_update_ne Eo Em n : ... @@ -112,12 +114,12 @@ Section lemmas. ... @@ -112,12 +114,12 @@ Section lemmas. Lemma aupd_acc Eo Em E α β Φ : Lemma aupd_acc Eo Em E α β Φ : Eo ⊆ E → Eo ⊆ E → atomic_update Eo Em α β Φ -∗ atomic_update Eo Em α β Φ -∗ atomic_step E (E∖Em) α (atomic_update Eo Em α β Φ) β Φ. atomic_acc E (E∖Em) α (atomic_update Eo Em α β Φ) β Φ. Proof using Type*. Proof using Type*. rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros (HE) "HUpd". rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros (HE) "HUpd". iPoseProof (greatest_fixpoint_unfold_1 with "HUpd") as "HUpd". iPoseProof (greatest_fixpoint_unfold_1 with "HUpd") as "HUpd". iDestruct "HUpd" as (P) "(HP & Hshift)". iDestruct "HUpd" as (P) "(HP & Hshift)". iRevert (E HE). iApply atomic_step_mask. iRevert (E HE). iApply atomic_acc_mask. iApply "Hshift". done. iApply "Hshift". done. Qed. Qed. ... @@ -132,7 +134,7 @@ Section lemmas. ... @@ -132,7 +134,7 @@ Section lemmas. Lemma aupd_intro P Q α β Eo Em Φ : Lemma aupd_intro P Q α β Eo Em Φ : Affine P → Persistent P → Laterable Q → Affine P → Persistent P → Laterable Q → (P ∗ Q -∗ atomic_step Eo (Eo∖Em) α Q β Φ) → (P ∗ Q -∗ atomic_acc Eo (Eo∖Em) α Q β Φ) → P ∗ Q -∗ atomic_update Eo Em α β Φ. P ∗ Q -∗ atomic_update Eo Em α β Φ. Proof. Proof. rewrite atomic_update_eq {1}/atomic_update_def /=. rewrite atomic_update_eq {1}/atomic_update_def /=. ... @@ -143,10 +145,10 @@ Section lemmas. ... @@ -143,10 +145,10 @@ Section lemmas. iApply HAU. by iFrame. iApply HAU. by iFrame. Qed. Qed. Lemma astep_intro x Eo Ei α P β Φ : Lemma aacc_intro x Eo Ei α P β Φ : Ei ⊆ Eo → α x -∗ Ei ⊆ Eo → α x -∗ ((α x ={Eo}=∗ P) ∧ (∀ y, β x y ={Eo}=∗ Φ x y)) -∗ ((α x ={Eo}=∗ P) ∧ (∀ y, β x y ={Eo}=∗ Φ x y)) -∗ atomic_step Eo Ei α P β Φ. atomic_acc Eo Ei α P β Φ. Proof. Proof. iIntros (?) "Hα Hclose". iIntros (?) "Hα Hclose". iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first set_solver. iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first set_solver. ... @@ -155,10 +157,10 @@ Section lemmas. ... @@ -155,10 +157,10 @@ Section lemmas. - iIntros (y) "Hβ". iMod "Hclose'" as "_". iApply "Hclose". done. - iIntros (y) "Hβ". iMod "Hclose'" as "_". iApply "Hclose". done. Qed. Qed. Global Instance elim_acc_astep {X} E1 E2 Ei (α' β' : X → PROP) γ' α β Pas Φ : Global Instance elim_acc_aacc {X} E1 E2 Ei (α' β' : X → PROP) γ' α β Pas Φ : ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ' ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ' (atomic_step E1 Ei α Pas β Φ) (atomic_acc E1 Ei α Pas β Φ) (λ x', atomic_step E2 Ei α (β' x' ∗ coq_tactics.maybe_wand (γ' x') Pas)%I β (λ x', atomic_acc E2 Ei α (β' x' ∗ coq_tactics.maybe_wand (γ' x') Pas)%I β (λ x y, β' x' ∗ coq_tactics.maybe_wand (γ' x') (Φ x y)))%I. (λ x y, β' x' ∗ coq_tactics.maybe_wand (γ' x') (Φ x y)))%I. Proof. Proof. rewrite /ElimAcc. rewrite /ElimAcc. ... @@ -179,14 +181,14 @@ Section lemmas. ... @@ -179,14 +181,14 @@ Section lemmas. iModIntro. destruct (γ' x'); iApply "HΦ"; done. iModIntro. destruct (γ' x'); iApply "HΦ"; done. Qed. Qed. Lemma astep_astep {A' B'} E1 E2 E3 Lemma aacc_aacc {A' B'} E1 E2 E3 α P β Φ α P β Φ (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) : (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) : atomic_step E1 E2 α P β Φ -∗ atomic_acc E1 E2 α P β Φ -∗ (∀ x, α x -∗ atomic_step E2 E3 α' (α x ∗ (P ={E1}=∗ P')) β' (∀ x, α x -∗ atomic_acc E2 E3 α' (α x ∗ (P ={E1}=∗ P')) β' (λ x' y', (α x ∗ (P ={E1}=∗ Φ' x' y')) (λ x' y', (α x ∗ (P ={E1}=∗ Φ' x' y')) ∨ ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗ ∨ ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗ atomic_step E1 E3 α' P' β' Φ'. atomic_acc E1 E3 α' P' β' Φ'. Proof. Proof. iIntros "Hupd Hstep". iMod ("Hupd") as (x) "[Hα Hclose]". iIntros "Hupd Hstep". iMod ("Hupd") as (x) "[Hα Hclose]". iMod ("Hstep" with "Hα") as (x') "[Hα' Hclose']". iMod ("Hstep" with "Hα") as (x') "[Hα' Hclose']". ... @@ -208,46 +210,46 @@ Section lemmas. ... @@ -208,46 +210,46 @@ Section lemmas. iApply "HΦ'". done. iApply "HΦ'". done. Qed. Qed. Lemma astep_aupd {A' B'} E1 E2 Eo Em Lemma aacc_aupd {A' B'} E1 E2 Eo Em α β Φ α β Φ (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) : (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) : Eo ⊆ E1 → Eo ⊆ E1 → atomic_update Eo Em α β Φ -∗ atomic_update Eo Em α β Φ -∗ (∀ x, α x -∗ atomic_step (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β' (∀ x, α x -∗ atomic_acc (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β' (λ x' y', (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ Φ' x' y')) (λ x' y', (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ Φ' x' y')) ∨ ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗ ∨ ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗ atomic_step E1 E2 α' P' β' Φ'. atomic_acc E1 E2 α' P' β' Φ'. Proof. Proof. iIntros (?) "Hupd Hstep". iApply (astep_astep with "[Hupd] Hstep"). iIntros (?) "Hupd Hstep". iApply (aacc_aacc with "[Hupd] Hstep"). iApply aupd_acc; done. iApply aupd_acc; done. Qed. Qed. Lemma astep_aupd_commit {A' B'} E1 E2 Eo Em Lemma aacc_aupd_commit {A' B'} E1 E2 Eo Em α β Φ α β Φ (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) : (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) : Eo ⊆ E1 → Eo ⊆ E1 → atomic_update Eo Em α β Φ -∗ atomic_update Eo Em α β Φ -∗ (∀ x, α x -∗ atomic_step (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β' (∀ x, α x -∗ atomic_acc (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β' (λ x' y', ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗ (λ x' y', ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗ atomic_step E1 E2 α' P' β' Φ'. atomic_acc E1 E2 α' P' β' Φ'. Proof. Proof. iIntros (?) "Hupd Hstep". iApply (astep_aupd with "Hupd"); first done. iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done. iIntros (x) "Hα". iApply atomic_step_wand; last first. iIntros (x) "Hα". iApply atomic_acc_wand; last first. { iApply "Hstep". done. } { iApply "Hstep". done. } iSplit; first by eauto. iIntros (??) "?". by iRight. iSplit; first by eauto. iIntros (??) "?". by iRight. Qed. Qed. Lemma astep_aupd_abort {A' B'} E1 E2 Eo Em Lemma aacc_aupd_abort {A' B'} E1 E2 Eo Em α β Φ α β Φ (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) : (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) : Eo ⊆ E1 → Eo ⊆ E1 → atomic_update Eo Em α β Φ -∗ atomic_update Eo Em α β Φ -∗ (∀ x, α x -∗ atomic_step (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β' (∀ x, α x -∗ atomic_acc (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β' (λ x' y', α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ Φ' x' y'))) -∗ (λ x' y', α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ Φ' x' y'))) -∗ atomic_step E1 E2 α' P' β' Φ'. atomic_acc E1 E2 α' P' β' Φ'. Proof. Proof. iIntros (?) "Hupd Hstep". iApply (astep_aupd with "Hupd"); first done. iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done. iIntros (x) "Hα". iApply atomic_step_wand; last first. iIntros (x) "Hα". iApply atomic_acc_wand; last first. { iApply "Hstep". done. } { iApply "Hstep". done. } iSplit; first by eauto. iIntros (??) "?". by iLeft. iSplit; first by eauto. iIntros (??) "?". by iLeft. Qed. Qed. ... @@ -264,13 +266,13 @@ Section proof_mode. ... @@ -264,13 +266,13 @@ Section proof_mode. Timeless (PROP:=PROP) emp → Timeless (PROP:=PROP) emp → TCForall Laterable (env_to_list Γs) → TCForall Laterable (env_to_list Γs) → P = prop_of_env Γs → P = prop_of_env Γs → envs_entails (Envs Γp Γs n) (atomic_step Eo (Eo∖Em) α P β Φ) → envs_entails (Envs Γp Γs n) (atomic_acc Eo (Eo∖Em) α P β Φ) → envs_entails (Envs Γp Γs n) (atomic_update Eo Em α β Φ). envs_entails (Envs Γp Γs n) (atomic_update Eo Em α β Φ). Proof. Proof. intros ? HΓs ->. rewrite envs_entails_eq of_envs_eq' /atomic_step /=. intros ? HΓs ->. rewrite envs_entails_eq of_envs_eq' /atomic_acc /=. setoid_rewrite prop_of_env_sound =>HAU. setoid_rewrite prop_of_env_sound =>HAU. apply aupd_intro; [apply _..|]. done. apply aupd_intro; [apply _..|]. done. Qed. Qed. End proof_mode. End proof_mode. (** Now the coq-level tactics *) (** Now the coq-level tactics *) ... ...
 ... @@ -29,18 +29,18 @@ Section increment. ... @@ -29,18 +29,18 @@ Section increment. iIntros (Q Φ) "HQ AU". iLöb as "IH". wp_let. iIntros (Q Φ) "HQ AU". iLöb as "IH". wp_let. wp_apply (load_spec with "[HQ]"); first by iAccu. wp_apply (load_spec with "[HQ]"); first by iAccu. (* Prove the atomic shift for load *) (* Prove the atomic shift for load *) iAuIntro. iApply (astep_aupd_abort with "AU"); first done. iAuIntro. iApply (aacc_aupd_abort with "AU"); first done. iIntros (x) "H↦". iIntros (x) "H↦". iApply (astep_intro (_, _) with "[H↦]"); [solve_ndisj|done|iSplit]. iApply (aacc_intro (_, _) with "[H↦]"); [solve_ndisj|done|iSplit]. { iIntros "\$ !> \$ !> //". } { iIntros "\$ !> \$ !> //". } iIntros ([]) "\$ !> AU !> HQ". iIntros ([]) "\$ !> AU !> HQ". (* Now go on *) (* Now go on *) wp_let. wp_op. wp_bind (aheap.(cas) _)%I. wp_let. wp_op. wp_bind (aheap.(cas) _)%I. wp_apply (cas_spec with "[HQ]"); first by iAccu. wp_apply (cas_spec with "[HQ]"); first by iAccu. (* Prove the atomic shift for CAS *) (* Prove the atomic shift for CAS *) iAuIntro. iApply (astep_aupd with "AU"); first done. iAuIntro. iApply (aacc_aupd with "AU"); first done. iIntros (x') "H↦". iIntros (x') "H↦". iApply (astep_intro with "[H↦]"); [solve_ndisj|done|iSplit]. iApply (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit]. { iIntros "\$ !> \$ !> //". } { iIntros "\$ !> \$ !> //". } iIntros ([]) "H↦ !>". iIntros ([]) "H↦ !>". destruct (decide (#x' = #x)) as [[= ->]|Hx]. destruct (decide (#x' = #x)) as [[= ->]|Hx]. ... @@ -70,7 +70,7 @@ Section increment_client. ... @@ -70,7 +70,7 @@ Section increment_client. iAssert (□ WP incr primitive_atomic_heap #l {{ _, True }})%I as "#Aupd". iAssert (□ WP incr primitive_atomic_heap #l {{ _, True }})%I as "#Aupd". { iAlways. wp_apply (incr_spec with "[]"); first by iAccu. clear x. { iAlways. wp_apply (incr_spec with "[]"); first by iAccu. clear x. iAuIntro. iInv nroot as (x) ">H↦". iAuIntro. iInv nroot as (x) ">H↦". iApply (astep_intro with "[H↦]"); [solve_ndisj|done|iSplit]. iApply (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit]. { by eauto 10. } { by eauto 10. } iIntros ([]) "H↦ !>". iSplitL "H↦"; first by eauto 10. iIntros ([]) "H↦ !>". iSplitL "H↦"; first by eauto 10. (* The continuation: From after the atomic triple to the postcondition of the WP *) (* The continuation: From after the atomic triple to the postcondition of the WP *) ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!