Commit 8ca249fb authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Use fractional pointers with extensional variable

parent 18fe6f53
......@@ -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
......@@ -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 xs2 as [|x2' xs2'].
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 xs2) "(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 xs2 as [|x2' xs2']; 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.
......
......@@ -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 :=
......
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