From 4107a2389fc64e4ead85c718166fff5e1073412a Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 25 Jan 2019 11:35:46 +0100 Subject: [PATCH] prettify treiber stack --- theories/logatom/treiber.v | 60 +++++++++++++++++--------------------- 1 file changed, 27 insertions(+), 33 deletions(-) diff --git a/theories/logatom/treiber.v b/theories/logatom/treiber.v index d2d2297..a897373 100644 --- a/theories/logatom/treiber.v +++ b/theories/logatom/treiber.v @@ -87,87 +87,81 @@ Section proof. Proof. generalize hd. induction xs; apply _. Qed. Lemma new_stack_spec: - ∀ (Φ: val → iProp Σ), - (∀ s, is_stack s [] -∗ Φ #s) ⊢ WP new_stack #() {{ Φ }}. + {{{ True }}} new_stack #() {{{ s, RET #s; is_stack s [] }}}. Proof. - iIntros (Φ) "HΦ". wp_lam. + iIntros (Φ) "_ HΦ". wp_lam. wp_bind (ref NONE)%E. wp_alloc l as "Hl". wp_alloc l' as "Hl'". iApply "HΦ". rewrite /is_stack. iExists l. iFrame. by iExists 1%Qp. Qed. - - Definition push_triple (s: loc) (x: val) := - <<< ∀ (xs : list val) (hd : loc), s ↦ #hd ∗ is_list hd xs >>> - push #s x @ ⊤ - <<< ∃ hd' : loc, s ↦ #hd' ∗ hd' ↦ SOMEV (x, #hd) ∗ is_list hd xs, RET #() >>>. Lemma push_atomic_spec (s: loc) (x: val) : - push_triple s x. + <<< ∀ (xs : list val), is_stack s xs >>> + push #s x @ ⊤ + <<< is_stack s (x::xs), RET #() >>>. Proof. - rewrite /push_triple. iApply wp_atomic_intro. + iApply wp_atomic_intro. unfold is_stack. iIntros (Φ) "HP". iLöb as "IH". wp_rec. wp_let. wp_bind (! _)%E. - iMod "HP" as (xs hd) "[[Hs Hhd] [Hvs' _]]". - wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame. + iMod "HP" as (xs) "[Hxs [Hvs' _]]". + iDestruct "Hxs" as (hd) "[Hs Hhd]". + wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by eauto with iFrame. iModIntro. wp_let. wp_alloc l as "Hl". wp_let. wp_bind (CAS _ _ _)%E. - iMod "HP" as (xs' hd') "[[Hs Hhd'] Hvs']". + iMod "HP" as (xs') "[Hxs' Hvs']". + iDestruct "Hxs'" as (hd') "[Hs' Hhd']". destruct (decide (hd = hd')) as [->|Hneq]. * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']". iMod ("Hvs'" with "[-]") as "HQ". - { by iFrame. } + { by eauto with iFrame. } iModIntro. wp_if. eauto. * wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]". - iMod ("Hvs'" with "[-]") as "HP"; first by iFrame. + iMod ("Hvs'" with "[-]") as "HP"; first by eauto with iFrame. iModIntro. wp_if. by iApply "IH". Qed. - Definition pop_triple (s: loc) := - <<< ∀ (xs : list val) (hd : loc), s ↦ #hd ∗ is_list hd xs >>> + Lemma pop_atomic_spec (s: loc) : + <<< ∀ (xs : list val), is_stack s xs >>> pop #s @ ⊤ - <<< match xs with [] => s ↦ #hd ∗ is_list hd [] - | x::xs' => ∃ q (hd': loc), hd ↦{q} SOMEV (x, #hd') ∗ s ↦ #hd' ∗ is_list hd' xs' end, + <<< match xs with [] => is_stack s [] + | x::xs' => is_stack s xs' end, RET match xs with [] => NONEV | x :: _ => SOMEV x end >>>. - - Lemma pop_atomic_spec (s: loc): - pop_triple s. Proof. - rewrite /pop_triple. iApply wp_atomic_intro. + iApply wp_atomic_intro. unfold is_stack. iIntros (Φ) "HP". iLöb as "IH". wp_rec. wp_bind (! _)%E. - iMod "HP" as (xs hd) "[[Hs Hhd] Hvs']". + iMod "HP" as (xs) "[Hxs Hvs']". + iDestruct "Hxs" as (hd) "[Hs Hhd]". destruct xs as [|y' xs']. - simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']". iDestruct "Hhd" as (q) "[Hhd Hhd']". iMod ("Hvs'" with "[-Hhd]") as "HQ". - { iFrame. eauto. } + { eauto with iFrame. } iModIntro. wp_let. wp_load. wp_pures. eauto. - simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')". iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame. wp_load. iDestruct "Hvs'" as "[Hvs' _]". iMod ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP". - { iFrame. iExists hd', (q / 2)%Qp. by iFrame. } + { eauto with iFrame. } iModIntro. wp_let. wp_load. wp_match. wp_proj. wp_bind (CAS _ _ _). - iMod "HP" as (xs hd'') "[[Hs Hhd''] Hvs']". + iMod "HP" as (xs'') "[Hxs'' Hvs']". + iDestruct "Hxs''" as (hd'') "[Hs'' Hhd'']". destruct (decide (hd = hd'')) as [->|Hneq]. + wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']". - destruct xs as [|x' xs'']. + destruct xs'' as [|x'' xs'']. { simpl. iDestruct "Hhd''" as (?) "H". iExFalso. by iDestruct (@mapsto_agree with "[\$Hhd1] [\$H]") as %?. } simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')". iDestruct (@mapsto_agree with "[\$Hhd1] [\$Hhd'']") as %[=]. subst. iMod ("Hvs'" with "[-]") as "HQ". - { iExists (q / 2 / 2)%Qp, _. - iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst. - repeat (iSplitR "Hxs1 Hs"; first done). - iFrame. } + { eauto with iFrame. } iModIntro. wp_if. wp_pures. eauto. + wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]". - iMod ("Hvs'" with "[-]") as "HP"; first by iFrame. + iMod ("Hvs'" with "[-]") as "HP"; first by eauto with iFrame. iModIntro. wp_if. by iApply "IH". Qed. End proof. -- GitLab