diff --git a/theories/logrel/F_mu_ref_conc/examples/queue/common.v b/theories/logrel/F_mu_ref_conc/examples/queue/common.v index 36e402d9b1b97fad3fda60347af3f47eb33a2b4e..9fb6a017db9483978dbd54b7aee1a5e879dfca4c 100644 --- a/theories/logrel/F_mu_ref_conc/examples/queue/common.v +++ b/theories/logrel/F_mu_ref_conc/examples/queue/common.v @@ -58,9 +58,43 @@ Section common. iIntros. iApply (own_update with "[$]"). by apply cmra_update_exclusive. Qed. + Lemma mapsto_full_to_frac l v : l ↦ᵢ v -∗ l ↦ᵢ{-} v. + Proof. iIntros. by iExists _. Qed. + + Lemma mapsto_full_to_frac_2 l v : l ↦ᵢ v -∗ l ↦ᵢ{-} v ∗ l ↦ᵢ{-} v. + Proof. + iIntros. iDestruct (mapsto_full_to_frac with "[$]") as "H". + iDestruct (mapsto_frac_duplicable with "H") as "[H1 H2]". + iFrame. + Qed. + + Lemma mapsto_full_to_frac_3 l v : l ↦ᵢ v -∗ (l ↦ᵢ{-} v ∗ l ↦ᵢ{-} v ∗ l ↦ᵢ{-} v). + Proof. + iIntros. + iDestruct (mapsto_full_to_frac_2 with "[$]") as "[H1 H2]". + iDestruct (mapsto_frac_duplicable with "H2") as "[H2 H3]". + iFrame. + Qed. + + Lemma mapsto_agree_frac l q v1 v2 : l ↦ᵢ{q} v1 -∗ l ↦ᵢ{-} v2 -∗ ⌜v1 = v2⌝. + Proof. + iIntros "P1". iDestruct 1 as (q2) "P2". iApply (mapsto_agree with "P1 P2"). + Qed. + + Lemma mapsto_agree_frac_frac l v1 v2 : l ↦ᵢ{-} v1 -∗ l ↦ᵢ{-} v2 -∗ ⌜v1 = v2⌝. + Proof. + iDestruct 1 as (q1) "P1". iDestruct 1 as (q2) "P2". + iApply (mapsto_agree with "P1 P2"). + Qed. + (* Maybe commit this upstream. *) Lemma mapsto_exclusive l v1 v2 q : l ↦ᵢ v1 -∗ l ↦ᵢ{q} v2 -∗ False. iIntros "Hl1 Hl2". iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[]%Qp_not_plus_q_ge_1. Qed. + Lemma mapsto_exclusive_frac l v1 v2 : l ↦ᵢ v1 -∗ l ↦ᵢ{-} v2 -∗ False. + iIntros "Hl1 Hl2". iDestruct "Hl2" as (q) "Hl2". + iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[]%Qp_not_plus_q_ge_1. + Qed. + End common. \ No newline at end of file diff --git a/theories/logrel/F_mu_ref_conc/examples/queue/refinement.v b/theories/logrel/F_mu_ref_conc/examples/queue/refinement.v index 224a9e74a8f74e6a366273b08c438418eb956c0e..e6ef45755328200869116288c0b46975bd0a49b4 100644 --- a/theories/logrel/F_mu_ref_conc/examples/queue/refinement.v +++ b/theories/logrel/F_mu_ref_conc/examples/queue/refinement.v @@ -69,25 +69,24 @@ Section Queue_refinement. *) Fixpoint isNodeList γ κ (ℓ : loc) (xs : list val) : iProp Σ := match xs with - | nil => ∃ ℓ2 q, ℓ ↦ᵢ{1/2} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{q} FoldV noneV ∗ own γ (◓ ℓ) + | nil => ∃ ℓ2, ℓ ↦ᵢ{1/2} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{-} FoldV noneV ∗ own γ (◓ ℓ) | x :: xs' => - (∃ ℓ2 ℓnext q ι, + (∃ ℓ2 ℓnext ι, own κ (◯ {[ ℓ2 := to_agree (ι, ℓnext) ]}) ∗ own ι (●{1/2} nodeLive) - ∗ ℓ ↦ᵢ{q} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV ℓnext))) + ∗ ℓ ↦ᵢ{-} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{-} FoldV (someV (PairV (InjRV x) (LocV ℓnext))) ∗ isNodeList γ κ ℓnext xs') end. Definition nextNode γ κ ℓinto : iProp Σ := ∃ ℓn, ((* node is nil *) - ∃ q, - ℓinto ↦ᵢ{1/2} (LocV ℓn) ∗ (* We own half the pointer into the node. *) - ℓn ↦ᵢ{q} (FoldV noneV) ∗ - own γ (◓ ℓinto)) (* Proof that ℓp is the actual pointer to nil in the queue. *) + ℓinto ↦ᵢ{1/2} (LocV ℓn) ∗ (* We own half the pointer into the node. *) + ℓn ↦ᵢ{-} (FoldV noneV) ∗ + own γ (◓ ℓinto)) (* Proof that ℓp is the actual pointer to nil in the queue. *) ∨ ((* non-nil *) - ∃ q ιnext ℓnext, - ℓinto ↦ᵢ{q} LocV ℓn ∗ + ∃ ιnext ℓnext, + ℓinto ↦ᵢ{-} LocV ℓn ∗ node_mapsto κ ℓn ιnext ℓnext ). @@ -96,13 +95,13 @@ Section Queue_refinement. ℓn is the "start" pointer of the node. *) Definition sentinelInv γ κ ι (ℓq ℓn ℓtoNext : loc) : iProp Σ := - ∃ q x, - ℓn ↦ᵢ{q} FoldV (someV (PairV x (LocV ℓtoNext))) ∗ + ∃ x, + ℓn ↦ᵢ{-} FoldV (someV (PairV x (LocV ℓtoNext))) ∗ nextNode γ κ ℓtoNext ∗ ((* ℓ is dead. It has been the sentinel, but no longer is. *) (own ι (● nodeDead) ∗ (* We know that the node points to a non-nil node. *) - ∃ q' x' b ℓnext, ℓtoNext ↦ᵢ{q'} LocV ℓnext ∗ ℓnext ↦ᵢ{q'} FoldV (someV (PairV x' b))) + ∃ x' b ℓnext, ℓtoNext ↦ᵢ{-} LocV ℓnext ∗ ℓnext ↦ᵢ{-} FoldV (someV (PairV x' b))) ∨ (* ℓn is currently the sentinel. *) (own ι (●{1/2} nodeSentinel) ∗ ℓq ↦ᵢ{1/2} (LocV ℓn)) (* We own half the pointer into the sentinel. *) @@ -277,17 +276,18 @@ Section Queue_refinement. ∃ ι, own κ (● (to_agree <$> (<[ℓnode := (ι, ℓtail)]> m)) : nodeUR) ∗ ▷ map_map γ κ ℓq (delete ℓsentinel (<[ℓnode := (ι, ℓtail)]>m)) ∗ - ℓnode ↦ᵢ{1/2} (FoldV (InjRV (PairV (InjRV x) (LocV ℓtail)))) ∗ + ℓnode ↦ᵢ{-} (FoldV (InjRV (PairV (InjRV x) (LocV ℓtail)))) ∗ isNodeList γ κ ℓhdPt (xs ++ [x]) ∗ node_mapsto κ ℓnode ι ℓtail ∗ - ℓ ↦ᵢ{1/2} (LocV ℓnode) + ℓ ↦ᵢ{-} (LocV ℓnode) }}}. Proof. iIntros (ϕ) "(% & authM & bigSep & #nodesInv & nilPts & tailPts & nodePts & nodeList & ℓPts & tok) Hϕ". iInduction xs as [|x' xs'] "IH" forall (ℓhdPt). - - iDestruct "nilPts" as "[nilPts nilPts']". + - iDestruct (mapsto_full_to_frac_2 with "nilPts") as "(nilPts & nilPts')". + (* iDestruct (mapsto_full_to_frac_2 with "tailPts") as "(tailPts & tailPts')". *) iDestruct "tailPts" as "[tailPts tailPts']". - iDestruct "nodeList" as (ℓ0 q) ">(ℓhdPt & ℓ0Pts &tok')". + iDestruct "nodeList" as (ℓ0) ">(ℓhdPt & ℓ0Pts &tok')". (* We need to be able to conclude that ℓhdPt is equal to ℓ. *) iDestruct (fracAgree_agree with "tok tok'") as %<-. iDestruct (mapsto_combine with "ℓhdPt ℓPts") as "[ℓpts %]". @@ -300,26 +300,29 @@ Section Queue_refinement. { iDestruct (big_sepM_lookup with "bigSep") as "conj". { rewrite lookup_delete_ne; done. } iDestruct "conj" as (ι0 ℓn) "(>-> & sentInv)". - iDestruct "sentInv" as (v' q0) "(>nodePts' & _)". - iDestruct (mapsto_exclusive with "nodePts nodePts'") as %[]. } - iDestruct "nodePts" as "[nodePts [nodePts' nodePts'']]". + iDestruct "sentInv" as (v') "(>nodePts' & _)". + iDestruct (mapsto_exclusive_frac with "nodePts nodePts'") as %[]. } + iDestruct (mapsto_full_to_frac_3 with "nodePts") as "(nodePts & nodePts' & nodePts'')". + (* iDestruct "nodePts" as "[nodePts [nodePts' nodePts'']]". *) iMod (insert_node_subset _ _ _ _ _ _ m (delete ℓsentinel m) with "[%] [% //] authM bigSep [authNodeState' nodePts'' tok tailPts' nilPts']") as "(authM & bigSep & #frag)". { apply delete_subseteq. } - { iExists _, _. iFrame "nodePts''". + { iExists _. iFrame "nodePts''". iSplitL "tailPts' nilPts' tok"; iExistsFrame. } iApply (wp_cas_suc with "ℓpts"). - iNext. iIntros "[[ℓpts _] [ℓpts' ℓpts'']]". + iNext. iIntros "ℓpts". + iDestruct (mapsto_full_to_frac_3 with "ℓpts") as "(ℓpts & ℓpts' & ℓpts'')". iApply "Hϕ". iExists _. rewrite delete_insert_ne; last done. iFrame "frag nodePts". iFrame. simpl. iExistsN. iFrame "frag nodePts'". iFrame. - iFrame. iExists _, _. iFrame "tailPts". iFrame. - - iDestruct "nodeList" as (ℓ0 ℓnext q ι) "(FOO & BAR & BAZ & HIHI & nodeListTail)". + iFrame. iExists _. iFrame "tailPts". iFrame. + - iDestruct "nodeList" as (ℓ0 ℓnext ι) "(FOO & BAR & BAZ & HIHI & nodeListTail)". iApply ("IH" with "authM bigSep nilPts tailPts nodePts nodeListTail ℓPts tok"). iNext. - iDestruct 1 as (ι') "(authM & bigSep & nilPts & tailPts & nodePts & nodeListTail & ℓPts)". + iDestruct 1 as (ι') "(authM & bigSep & nilPts & tailPts & nodePts & ℓPts)". + (* iDestruct 1 as (ι') "(authM & bigSep & nilPts & tailPts & nodePts & nodeListTail & ℓPts)". *) iApply "Hϕ". iExistsFrame. Qed. @@ -366,7 +369,8 @@ Section Queue_refinement. iNext. iIntros (tail) "[tailPts tailPts'] /=". iApply wp_value. iApply wp_alloc; first done. iNext. - iIntros (ℓsentinel) "[sentinelPts sentinelPts'] /=". + iIntros (ℓsentinel) "sentinelPts /=". + iDestruct (mapsto_full_to_frac_2 with "sentinelPts") as "(sentinelPts & sentinelPts')". iApply wp_alloc; first done. iNext. iIntros (ℓq) "[qPts qPts'] /=". iApply wp_pure_step_later; auto. iNext. @@ -388,7 +392,7 @@ Section Queue_refinement. { rewrite map_fmap_singleton. iAssumption. } rewrite /map_map big_sepM_singleton. iExistsN. iSplit; auto. - iExists (1/2)%Qp, _. iFrame "sentinelPts'". + iExists _. iFrame "sentinelPts'". iSplitL "tailPts nilPts token1"; iExistsFrame. } iMod (inv_alloc queueN _ (queueInv _ _ τi ℓq list _) with "[qPts lockPts listPts' sentinelPts tailPts' nilPts' token2 authNodeSentinel fragO]") @@ -426,9 +430,9 @@ Section Queue_refinement. iApply (wp_bind (fill [UnfoldCtx; CaseCtx _ _])). iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv". iDestruct (node_lookup with "authM bigSep fragO") as "(sentInv & authM & bigSep)". - iDestruct "sentInv" as (q x) "([sentinelPts sentinelPts'] & nextNode & rest)". - iApply (wp_load with "sentinelPts"). - iNext. iIntros "sentinelPts". + iDestruct "sentInv" as (x) "(>sentinelPts & nextNode & rest)". + iDestruct (mapsto_frac_duplicable with "sentinelPts") as "(sentinelPts & sentinelPts')". + iApply (wp_load_frac with "sentinelPts"). iNext. iIntros "sentinelPts". iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' nextNode rest]") as "(authM & bigSep)". { iExistsFrame. } iMod ("closeNodesInv" with "[authM bigSep]") as "_". { iExistsFrame. } @@ -450,16 +454,16 @@ Section Queue_refinement. iApply wp_value. simpl. iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv". iDestruct (node_lookup with "authM bigSep fragO") as "(sentInv & authM & bigSep)". - iDestruct "sentInv" as (q' x') "(sentinelPts' & next & disj)". + iDestruct "sentInv" as (x') "(sentinelPts' & next & disj)". iDestruct "next" as (ℓn) "[Left | Right]". + (* xs is the empty list *) - iDestruct "Left" as (q0) ">(hdPtPts & [nPts nPts'] & tok)". - simpl. + iDestruct "Left" as ">(hdPtPts & nPts & tok)". + iDestruct (mapsto_frac_duplicable with "nPts") as "(nPts & nPts')". iDestruct "disj" as "[>[_ pts] | [sent | >live]]". 1: { - iDestruct "pts" as (q1 x1 b ℓnext) "(hdPtPts' & nextPts)". - iDestruct (mapsto_agree with "hdPtPts hdPtPts'") as %[= ->]. - iDestruct (mapsto_agree with "nPts nextPts") as %[=]. + iDestruct "pts" as (x1 b ℓnext) "(hdPtPts' & nextPts)". + iDestruct (mapsto_agree_frac with "hdPtPts hdPtPts'") as %[= ->]. + iDestruct (mapsto_agree_frac_frac with "nPts nextPts") as %[=]. } 2: { iDestruct (state_leq with "live nodeState") as %le. inversion le. } iDestruct "sent" as ">(authState & qPts)". @@ -476,9 +480,9 @@ Section Queue_refinement. not a nil the queue cannot be empty. *) destruct xs2 as [|x2 xs2']. 2: { - iDestruct "nodeList" as (ℓ2 next q1 ι0) "(_ & _ & >hdPtPts' & >ℓ2Pts & _)". - iDestruct (mapsto_agree with "hdPtPts hdPtPts'") as %[= <-]. - iDestruct (mapsto_agree with "nPts ℓ2Pts") as %[=]. + iDestruct "nodeList" as (ℓ2 next ι0) "(_ & _ & >hdPtPts' & >ℓ2Pts & _)". + iDestruct (mapsto_agree_frac with "hdPtPts hdPtPts'") as %[= <-]. + iDestruct (mapsto_agree_frac_frac with "nPts ℓ2Pts") as %[=]. } destruct xsₛ2 as [|x2' xsₛ2']. 2: { iDestruct (big_sepL2_length with "Hlink") as ">%". inversion H6. } @@ -496,7 +500,7 @@ Section Queue_refinement. iMod ("closeNodesInv" with "[authM bigSep]") as "_". { iNext. iExistsFrame. } iModIntro. - iApply (wp_load with "nPts"). iNext. iIntros "otherPts". + iApply (wp_load_frac with "nPts"). iNext. iIntros "otherPts". iApply wp_pure_step_later; auto. iNext. simpl. iApply wp_value. simpl. iApply wp_pure_step_later; auto. iNext. simpl. @@ -504,8 +508,9 @@ Section Queue_refinement. iExists (noneV). iFrame. iLeft. iExists (_, _). simpl. done. + (* xs is not the empty list *) - iDestruct "Right" as (q0 ι2 next) "(>[hdPtPts hdPtPts'] & #nextMapsto)". - iApply (wp_load with "[$hdPtPts]"). iNext. iIntros "hdPtPts". + iDestruct "Right" as (ι2 next) "(>hdPtPts & #nextMapsto)". + iDestruct (mapsto_frac_duplicable with "hdPtPts") as "(hdPtPts & hdPtPts')". + iApply (wp_load_frac with "[$hdPtPts]"). iNext. iIntros "hdPtPts". simpl. iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' disj hdPtPts']") as "(authM & bigSep)". { iExistsFrame. } @@ -514,8 +519,9 @@ Section Queue_refinement. iModIntro. clear m. iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv". iDestruct (node_lookup with "authM bigSep nextMapsto") as "(nextInv & authM & bigSep)". - iDestruct "nextInv" as (q2 x2) "([otherPts otherPts'] & rest)". - iApply (wp_load with "[$otherPts]"). iNext. iIntros "otherPts". + iDestruct "nextInv" as (x2) "(otherPts & rest)". + iDestruct (mapsto_frac_duplicable with "otherPts") as "[otherPts otherPts']". + iApply (wp_load_frac with "[$otherPts]"). iNext. iIntros "otherPts". simpl. iDestruct (reinsert_node with "authM nextMapsto bigSep [otherPts' rest]") as "(authM & bigSep)". { iExistsFrame. } @@ -531,7 +537,7 @@ Section Queue_refinement. iApply (wp_bind (fill [LoadCtx])). iApply wp_pure_step_later; auto. iNext. iApply wp_value. simpl. - iApply (wp_load with "hdPtPts"). iNext. iIntros "hdPtPts". + iApply (wp_load_frac with "hdPtPts"). iNext. iIntros "hdPtPts". simpl. iInv queueN as (xs2 xsₛ2) "(isMSQ & Hsq & lofal & Hlink)" "Hclose". rewrite /isMSQueue. @@ -540,7 +546,7 @@ Section Queue_refinement. (* We now open the nodes invariant. *) iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv". iDestruct (node_lookup with "authM bigSep fragO'") as "(sentInv & authM & bigSep)". - iDestruct "sentInv" as (v3 q3) "(>sentinelPts' & next & [[>ownO _]|[>snd| >ownO]])"; + iDestruct "sentInv" as (v3) "(>sentinelPts' & next & [[>ownO _]|[>snd| >ownO]])"; try iDestruct (state_agree with "sentinelState ownO") as %[=]. iDestruct "snd" as "(ownO & qPts2)". iCombine "sentinelState ownO" as "sentinelState". @@ -555,17 +561,17 @@ Section Queue_refinement. still points to the same sentinel a lot of the existential variables we receieved the first time around are equal to the ones we have now. Establishing this is critical. *) - iDestruct (mapsto_agree with "sentinelPts sentinelPts'") as %[= <- <-]. + iDestruct (mapsto_agree_frac_frac with "sentinelPts sentinelPts'") as %[= <- <-]. (* xs2 is not necessarily equal to xs, but, since the CAS succeeded, it still has xs as a prefix. And since we know that xs is a cons xs2 must also be a cons with the same element. *) destruct xs2 as [|x2' xs2']; simpl. - { iDestruct "nodeList" as (ℓ2 q1) "(ℓhdPts & ℓ2Pts & tok)". - iDestruct (mapsto_agree with "ℓhdPts hdPtPts") as %[= ->]. - iDestruct (mapsto_agree with "otherPts ℓ2Pts") as %[=]. } + { iDestruct "nodeList" as (ℓ2) "(ℓhdPts & ℓ2Pts & tok)". + iDestruct (mapsto_agree_frac with "ℓhdPts hdPtPts") as %[= ->]. + iDestruct (mapsto_agree_frac_frac with "otherPts ℓ2Pts") as %[=]. } destruct xsₛ2 as [|xₛ2' xsₛ2']; first done. - iDestruct "nodeList" as (ℓtail ℓnext q1 ι3) "(#frag & nodeState' & hdPtPts' & tailPts & nodeList)". - iDestruct (mapsto_agree with "hdPtPts hdPtPts'") as %[= ->]. + iDestruct "nodeList" as (ℓtail ℓnext ι3) "(#frag & nodeState' & hdPtPts' & tailPts & nodeList)". + iDestruct (mapsto_agree_frac_frac with "hdPtPts hdPtPts'") as %[= ->]. iAssert (⌜delete ℓsentinel m !! ℓtail = Some (ι3, ℓnext)⌝%I) as %Eq. { iDestruct (auth_node_mapsto_Some with "authM frag") as %Eq. destruct (decide (ℓsentinel = ℓtail)) as [->|Neq]. @@ -575,11 +581,11 @@ Section Queue_refinement. - iPureIntro. by apply lookup_delete_Some. } (* We lookup the current head of the list/new sentinel. *) iDestruct (big_sepM_delete with "bigSep") as "[conjunct bigSep]"; first apply Eq. - iDestruct "conjunct" as (ιtemp ℓtemp [= <- <-] q'' x'') "(hdPtPts'' & nn & [[st _]|[[st _]|st]])"; + iDestruct "conjunct" as (ιtemp ℓtemp [= <- <-] x'') "(hdPtPts'' & nn & [[st _]|[[st _]|st]])"; try iDestruct (state_agree with "st nodeState'") as %[=]. iCombine "nodeState' st" as "nodeState'". iMod (update_live_sentinel with "nodeState'") as "[nodeState1 nodeState2]". - iDestruct (mapsto_agree with "otherPts tailPts") as %[= -> ->]. + iDestruct (mapsto_agree_frac_frac with "otherPts tailPts") as %[= -> ->]. iDestruct "Hlink" as "[Hτi Hlink]". (* We step through the specificaion code. *) iMod (steps_CG_dequeue_cons with "[$Hspec $Hj $Hsq $lofal]") as "(Hj & Hsq & lofal)". @@ -594,8 +600,8 @@ Section Queue_refinement. { iExistsFrame. } iDestruct (reinsert_node_Some with "bigSep [sentinelPts sentinelState hdPtPts' tailPts]") as "bigSep". { apply sentSome. } - { iDestruct "hdPtPts'" as "[hdPtPts1 hdPtPts2]". - iDestruct "tailPts" as "[tailPts1 tailPts2]". + { iDestruct (mapsto_frac_duplicable with "hdPtPts'") as "[hdPtPts1 hdPtPts2]". + iDestruct (mapsto_frac_duplicable with "tailPts") as "[tailPts tailPts2]". iExistsN. iFrame. iSplitL "hdPtPts1"; iExistsFrame. } iMod ("closeNodesInv" with "[authM bigSep]") as "_". { iNext. iExistsFrame. } @@ -667,8 +673,9 @@ Section Queue_refinement. (* Lookup node *) iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv". iDestruct (node_lookup with "authM bigSep fragO") as "(sentInv & authM & bigSep)". - iDestruct "sentInv" as (q x) "([sentinelPts sentinelPts'] & nextNode & rest)". - iApply (wp_load with "sentinelPts"). + iDestruct "sentInv" as (x) "(sentinelPts & nextNode & rest)". + iDestruct (mapsto_frac_duplicable with "sentinelPts") as "[sentinelPts sentinelPts']". + iApply (wp_load_frac with "sentinelPts"). iNext. iIntros "sentinelPts". simpl. iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' nextNode rest]") as "(authM & bigSep)". @@ -686,16 +693,17 @@ Section Queue_refinement. iApply wp_value. simpl. (* We are now done evaluating the argument. *) - iLöb as "Hlat" forall (x ι ℓhdPt ℓsentinel q) "fragO". + iLöb as "Hlat" forall (x ι ℓhdPt ℓsentinel) "fragO". iApply wp_pure_step_later; auto. iNext. iAsimpl. iApply (wp_bind (fill [LetInCtx _])). (* Lookup node *) iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv". iDestruct (node_lookup with "authM bigSep fragO") as "(sentInv & authM & bigSep)". - iDestruct "sentInv" as (q' x') "(sentinelPts' & next & rest)". + iDestruct "sentInv" as (x') "(sentinelPts' & next & rest)". iDestruct "next" as (ℓn) "[left | right]". + (* We are at the end and can attempt inserting our node. *) - iDestruct "left" as (q0) "(ℓPts & [ℓ2Pts ℓ2Pts'] & tok)". + iDestruct "left" as "(>ℓPts & >ℓ2Pts & tok)". + iDestruct (mapsto_frac_duplicable with "ℓ2Pts") as "(ℓ2Pts & ℓ2Pts')". iApply (wp_load with "ℓPts"). iNext. iIntros "ℓPts". simpl. iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' ℓPts ℓ2Pts' tok rest]") as "(authM & bigSep)". @@ -707,7 +715,7 @@ Section Queue_refinement. iApply (wp_bind (fill [CaseCtx _ _])). iApply (wp_bind (fill [UnfoldCtx])). simpl. - iApply (wp_load with "ℓ2Pts"). + iApply (wp_load_frac with "ℓ2Pts"). iNext. iIntros "ℓ2Pts". simpl. iApply wp_pure_step_later; auto; iNext. iApply wp_value. @@ -723,25 +731,24 @@ Section Queue_refinement. clear m. iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv". iDestruct (node_lookup with "authM bigSep fragO") as "(sentInv & authM & bigSep)". - iDestruct "sentInv" as (q2 x2) "(sentinelPts' & next & rest)". + iDestruct "sentInv" as (x2) "(sentinelPts' & next & rest)". iDestruct "next" as (ℓn') "disj". destruct (decide (ℓn' = ℓn)) as [|Hneq]; subst. * (* We are still at the end. *) iDestruct "disj" as "[left|right]". iAssert (⌜ℓsentinel ≠ ℓnode⌝%I) as %Neq. - { iIntros (->). iApply (mapsto_exclusive with "nodePts sentinelPts"). } + { iIntros (->). iApply (mapsto_exclusive_frac with "nodePts sentinelPts"). } (* The second case is a contradiction since we know that the node points to the same thing as before and we have investigated that node and found it to be a nil-node. *) 2: { - iDestruct "right" as (qT ιT next) "(>hdPts' & >#nextPts)". + iDestruct "right" as (ιT next) "(>hdPts' & >#nextPts)". iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts hdPts' rest]") as "(>authM & bigSep)". { iExistsFrame. } iDestruct (node_lookup with "authM bigSep nextPts") as "(nodeInv & authM & bigSep)". - iDestruct "nodeInv" as (q4 x4) "(>nPts & nextNode & rest)". - iDestruct (mapsto_agree with "nPts ℓ2Pts") as %[=]. - } - iDestruct "left" as (q3) ">(ℓPts & ℓ2Pts2 & tok)". + iDestruct "nodeInv" as (x3) "(>nPts & nextNode & rest)". + iDestruct (mapsto_agree_frac_frac with "nPts ℓ2Pts") as %[=]. } + iDestruct "left" as ">(ℓPts & ℓ2Pts2 & tok)". simpl. iApply (enqueue_cas with "[$authM $bigSep $nodesInv $nilPts $tailPts $nodePts $nodeList $ℓPts $tok]"). { done. } @@ -766,7 +773,7 @@ Section Queue_refinement. * (* Another thread changed the end in the meantime. *) iDestruct "disj" as "[left|right]". (* FIXME: There is quite a bit of duplicated code in the two cases below. *) - -- iDestruct "left" as (q1) ">(ℓPts & ℓ2Pts2 & tok)". + -- iDestruct "left" as ">(ℓPts & ℓ2Pts2 & tok)". iApply (wp_cas_fail with "ℓPts"). congruence. iNext. iIntros "ℓPts". iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' ℓPts ℓ2Pts2 tok rest]") as "(authM & bigSep)". @@ -781,8 +788,8 @@ Section Queue_refinement. iApply wp_pure_step_later; auto; iNext. iApply ("Hlat" $! _ _ ℓhdPt with "Hj nilPts tailPts nodePts sentinelPts"). iModIntro. done. - -- iDestruct "right" as (q3 x3 next) "(>ℓPts & nodeInvNext)". - iApply (wp_cas_fail with "ℓPts"). congruence. + -- iDestruct "right" as (x3 next) "(>ℓPts & nodeInvNext)". + iApply (wp_cas_fail_frac with "ℓPts"). congruence. iNext. iIntros "ℓPts". iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' ℓPts rest nodeInvNext]") as "(authM & bigSep)". { iExistsFrame. } @@ -797,9 +804,9 @@ Section Queue_refinement. iApply ("Hlat" $! _ _ ℓhdPt with "Hj nilPts tailPts nodePts sentinelPts"). iModIntro. done. + (* We are not at the end yet, keep on going. *) - iDestruct "right" as (q3 ι3 next) "(>ℓPts & #nodeInvNext)". + iDestruct "right" as (ι3 next) "(>ℓPts & #nodeInvNext)". (* iDestruct "right" as (x next) "(>[ℓPts ℓPts'] & [ℓ2Pts ℓ2Pts'] & #nodeInvNext)". *) - iApply (wp_load with "ℓPts"). + iApply (wp_load_frac with "ℓPts"). iNext. iIntros "ℓPts". simpl. iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts' ℓPts rest nodeInvNext]") as "(authM & bigSep)". { iExistsFrame. } @@ -812,8 +819,9 @@ Section Queue_refinement. clear m. iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv". iDestruct (node_lookup with "authM bigSep nodeInvNext") as "(nodeInv & authM & bigSep)". - iDestruct "nodeInv" as (q4 x4) "([nPts nPts'] & nextNode & rest)". - iApply (wp_load with "nPts"). + iDestruct "nodeInv" as (x4) "(nPts & nextNode & rest)". + iDestruct (mapsto_frac_duplicable with "nPts") as "(nPts & nPts')". + iApply (wp_load_frac with "nPts"). iNext. iIntros "nPts". simpl. iDestruct (reinsert_node with "authM nodeInvNext bigSep [nPts' nextNode rest]") as "(authM & bigSep)". { iExistsFrame. } @@ -827,7 +835,7 @@ Section Queue_refinement. simpl. iApply wp_pure_step_later; auto; iNext. simpl. iApply wp_value. simpl. - iApply ("Hlat" $! _ _ next ℓn _ with "Hj nilPts tailPts nodePts nPts [nodeInvNext]"). + iApply ("Hlat" $! _ _ next ℓn with "Hj nilPts tailPts nodePts nPts [nodeInvNext]"). iModIntro. done. Qed. diff --git a/theories/logrel/F_mu_ref_conc/rules.v b/theories/logrel/F_mu_ref_conc/rules.v index 6de572453c9c081a858077d3b912ad07d2a8aa28..a944eeb0362ad0ba841715edd6f21763f5f5cefd 100644 --- a/theories/logrel/F_mu_ref_conc/rules.v +++ b/theories/logrel/F_mu_ref_conc/rules.v @@ -24,6 +24,7 @@ Global Opaque iris_invG. Notation "l ↦ᵢ{ q } v" := (mapsto (L:=loc) (V:=val) l q v) (at level 20, q at level 50, format "l ↦ᵢ{ q } v") : bi_scope. Notation "l ↦ᵢ v" := (mapsto (L:=loc) (V:=val) l 1 v) (at level 20) : bi_scope. +Notation "l ↦ᵢ{-} v" := (∃ q, l ↦ᵢ{q} v)%I (at level 20, format "l ↦ᵢ{-} v") : bi_scope. Section lang_rules. Context `{heapIG Σ}. @@ -74,6 +75,14 @@ Section lang_rules. iModIntro; iSplit=> //. iFrame. by iApply "HΦ". Qed. + Lemma wp_load_frac E l v : + {{{ ▷ l ↦ᵢ{-} v }}} Load (Loc l) @ E {{{ RET v; l ↦ᵢ{-} v }}}. + Proof. + iIntros (Φ) ">Hl HΦ". iDestruct "Hl" as (q) "Hl". + iApply (wp_load with "Hl"). iNext. iIntros "Hl". + iApply "HΦ". by iExists q. + Qed. + Lemma wp_store E l v' e v : IntoVal e v → {{{ ▷ l ↦ᵢ v' }}} Store (Loc l) e @ E @@ -100,6 +109,16 @@ Section lang_rules. iModIntro; iSplit=> //. iFrame. by iApply "HΦ". Qed. + Lemma wp_cas_fail_frac E l v' e1 v1 e2 v2 : + IntoVal e1 v1 → IntoVal e2 v2 → v' ≠ v1 → + {{{ ▷ l ↦ᵢ{-} v' }}} CAS (Loc l) e1 e2 @ E + {{{ RET (BoolV false); l ↦ᵢ{-} v' }}}. + Proof. + iIntros (<- <- ? Φ) ">Hl HΦ". iDestruct "Hl" as (q) "Hl". + iApply (wp_cas_fail with "Hl"); first done. + iNext. iIntros "Hl". iApply "HΦ". by iExists q. + Qed. + Lemma wp_cas_suc E l e1 v1 e2 v2 : IntoVal e1 v1 → IntoVal e2 v2 → {{{ ▷ l ↦ᵢ v1 }}} CAS (Loc l) e1 e2 @ E @@ -121,6 +140,12 @@ Section lang_rules. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. by iFrame. Qed. + Lemma mapsto_frac_duplicable l v : + l ↦ᵢ{-} v -∗ l ↦ᵢ{-} v ∗ l ↦ᵢ{-} v. + Proof. + iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto. + Qed. + Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto. Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step. Local Ltac solve_pure_exec :=