Commit 6a8b08c5 authored by Simon Friis Vindum's avatar Simon Friis Vindum

Proove enqueue

parent 1ddb18f9
......@@ -8,41 +8,81 @@ From iris_examples.logrel.F_mu_ref_conc.examples.queue Require Import
From iris.proofmode Require Import tactics.
Definition queueN : namespace := nroot .@ "queue".
Definition nodeN : namespace := queueN .@ "node".
Definition nodeN : namespace := nroot .@ "node".
Definition fracAgreeR : cmraT := prodR fracR (agreeR (leibnizO loc)).
Section Queue_refinement.
Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}.
Context `{heapIG Σ, cfgSG Σ, inG Σ fracAgreeR}.
Notation D := (prodO valO valO -n> iPropO Σ).
Definition noneV := InjLV UnitV.
Definition someV v := InjRV v.
Program Definition nodeInv_pre : (valO -n> iPropO Σ) -n> (valO -n> iPropO Σ) :=
λne P n,
( 2 q, n = LocV ℓ⌝
(( ↦ᵢ{1/2} (LocV 2) 2 ↦ᵢ{q} FoldV (noneV))
( x next, ↦ᵢ{q} (LocV 2) 2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) next))
Local Notation "◓ v" := ((1/2)%Qp, to_agree v) (at level 20).
Lemma fracAgree_agree γ (q1 q2 : Qp) v1 v2 :
own γ (q1, to_agree v1)
- own γ (q2, to_agree v2)
- v1 = v2.
Proof.
iIntros "H1 H2".
iDestruct (own_valid_2 with "H1 H2") as %HValid.
destruct HValid as [_ H2].
iIntros "!%"; by apply agree_op_invL'.
Qed.
Lemma fracAgree_combine γ (q1 q2 : Qp) v1 v2 :
own γ (q1, to_agree v1)
- own γ (q2, to_agree v2)
- own γ ((q1 + q2)%Qp, to_agree v2) v1 = v2.
Proof.
iIntros "Hl1 Hl2".
iDestruct (fracAgree_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl".
iDestruct (own_valid with "Hl") as %Hv.
apply pair_valid in Hv.
eauto with iFrame.
Qed.
Lemma fracAgree_update γ v w u :
own γ ( v) - own γ ( w) == own γ (1%Qp, to_agree u).
Proof.
iIntros "Hb1 Hb2".
iDestruct (fracAgree_combine with "Hb1 Hb2") as "[tok <-]".
rewrite Qp_half_half.
iApply (own_update with "tok").
by apply cmra_update_exclusive.
Qed.
Definition locO := leibnizO loc. (* FIXME: This should be included in Iris? *)
Program Definition nodeInv_pre γ : (locO -n> iPropO Σ) -n> (locO -n> iPropO Σ) :=
λne P ,
( 2 q,
(( ↦ᵢ{1/2} (LocV 2) 2 ↦ᵢ{q} FoldV (noneV) own γ ( ))
( x next, ↦ᵢ{q} (LocV 2) 2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV next)))
inv nodeN (P next)))
)%I.
Solve Obligations with solve_proper.
Global Instance nodeInv_pre_contractive : Contractive (nodeInv_pre).
Global Instance nodeInv_pre_contractive : Contractive (nodeInv_pre γ).
Proof. solve_contractive. Qed.
Definition nodeInv : valO -n> iPropO Σ := fixpoint (nodeInv_pre).
Definition nodeInv γ : locO -n> iPropO Σ := fixpoint (nodeInv_pre γ).
Lemma nodeInv_unfold n :
nodeInv n (
2 q, n = LocV ℓ⌝
(( ↦ᵢ{1/2} (LocV 2) 2 ↦ᵢ{q} FoldV (noneV))
Lemma nodeInv_unfold γ :
nodeInv γ (
2 q,
(( ↦ᵢ{1/2} (LocV 2) 2 ↦ᵢ{q} FoldV (noneV) own γ ( ))
( x next, ↦ᵢ{q} (LocV 2) 2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) next))
inv nodeN (nodeInv next)))
( x next, ↦ᵢ{q} (LocV 2) 2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV next)))
inv nodeN (nodeInv γ next)))
)%I.
Proof. rewrite /nodeInv. apply (fixpoint_unfold nodeInv_pre n). Qed.
Proof. rewrite /nodeInv. apply (fixpoint_unfold (nodeInv_pre γ) ). Qed.
Fixpoint isCGQueue_go (xs : list val) : val :=
match xs with
......@@ -56,13 +96,13 @@ Section Queue_refinement.
(* Represents the information that the location ℓ points to a series of nodes
correscponding to the list `xs`.
*)
Fixpoint isNodeList q ( : loc) (xs : list val) : iProp Σ :=
Fixpoint isNodeList γ ( : loc) (xs : list val) : iProp Σ :=
match xs with
| nil => 2, ↦ᵢ{1/2} (LocV 2) 2 ↦ᵢ{q} FoldV noneV
| nil => 2 q, ↦ᵢ{1/2} (LocV 2) 2 ↦ᵢ{q} FoldV noneV own γ ( )
| x :: xs' =>
( 2 next,
( 2 next q,
↦ᵢ{q} (LocV 2) 2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV next)))
isNodeList q next xs')
isNodeList γ next xs')
end.
(* Represents that the location ℓ points to a series of nodes corresponding to
......@@ -70,45 +110,45 @@ Section Queue_refinement.
isNodeList is that this predicates does not say exactly what the end is,
i.e. the final node, is because this may change. Loosely speaking this
represent the persistent information in isNodeList. *)
Fixpoint firstXsValues q ( : loc) (xs : list val) : iProp Σ :=
Fixpoint firstXsValues ( : loc) (xs : list val) : iProp Σ :=
match xs with
| nil => True (* Here we should be able to say that ℓ is either another node or the end. *)
| x :: xs' =>
( 2 next, ↦ᵢ{q} (LocV 2) 2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV next)))
firstXsValues q next xs')
( 2 next q, ↦ᵢ{q} (LocV 2) 2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV next)))
firstXsValues next xs')
end.
Lemma firstXsValues_split q xs : firstXsValues q xs - firstXsValues (q/2) xs firstXsValues (q/2) xs : iProp Σ.
Lemma firstXsValues_split xs : firstXsValues xs - firstXsValues xs firstXsValues xs : iProp Σ.
Proof.
iIntros "H".
iInduction xs as [|x xs'] "IH" forall (); simpl.
- done.
- iDestruct "H" as (tail next) "([ℓPts1 ℓPts2] & [ℓtailPts1 ℓtailPts2] & Hnl)".
- iDestruct "H" as (tail next q) "([ℓPts1 ℓPts2] & [ℓtailPts1 ℓtailPts2] & Hnl)".
iDestruct ("IH" with "Hnl") as "[Ha Hb]".
iSplitL "ℓPts1 ℓtailPts1 Ha"; iExists _, _; iFrame.
iSplitL "ℓPts1 ℓtailPts1 Ha"; iExists _, _, _; iFrame.
Qed.
Lemma splitIsNodeList q xs : isNodeList q xs - isNodeList (q/2) xs firstXsValues (q/2) xs : iProp Σ.
Lemma splitIsNodeList γ xs : isNodeList γ xs - isNodeList γ xs firstXsValues xs : iProp Σ.
Proof.
iIntros "isNodeList".
(* generalize dependent ℓ. *)
iInduction xs as [|x xs'] "IH" forall (); simpl.
- iDestruct "isNodeList" as (2) "(ℓPts1 & [ℓtailPts1 ℓtailPts2] & Hnl)".
iSplit; auto. iExists _. iFrame.
- iDestruct "isNodeList" as (2 next) "([ℓPts1 ℓPts2] & [ℓtailPts1 ℓtailPts2] & Hnl)".
- iDestruct "isNodeList" as (2 q) "(ℓPts1 & [ℓtailPts1 ℓtailPts2] & Hnl)".
iSplit; auto. iExists _, _. iFrame.
- iDestruct "isNodeList" as (2 next q) "([ℓPts1 ℓPts2] & [ℓtailPts1 ℓtailPts2] & Hnl)".
iDestruct ("IH" with "Hnl") as "[Ha Hb]".
iSplitL "ℓPts1 ℓtailPts1 Ha"; iExists _, _; iFrame.
iSplitL "ℓPts1 ℓtailPts1 Ha"; iExists _, _, _; iFrame.
Qed.
(* Predicate expression that ℓ points to a queue with the values xs *)
Definition isMSQueue (τi : D) ( : loc) (xs : list val) : iProp Σ :=
( sentinel v hdPt q p,
Definition isMSQueue γ (τi : D) ( : loc) (xs : list val) : iProp Σ :=
( sentinel v hdPt q,
↦ᵢ (LocV sentinel)
sentinel ↦ᵢ{q} (FoldV (someV (PairV v (LocV hdPt))))
(* ∗ ℓhdPt ↦ᵢ{q} (LocV ℓhd) *)
isNodeList p hdPt xs
isNodeList γ hdPt xs
(* ∗ firstXsValues p ℓhd xsᵢ *)
inv nodeN (nodeInv (LocV hdPt))
inv nodeN (nodeInv γ hdPt)
)%I.
Fixpoint xsLink (τi : D) (xs xs : list val) : iProp Σ :=
......@@ -118,9 +158,22 @@ Section Queue_refinement.
| _ => False
end.
Definition invariant τi hd sHd lock: iProp Σ :=
Lemma xsLink_snoc τi xs xs v w :
xsLink τi xs xs - τi (v, w) - xsLink τi (xs ++ [v]) (xs ++ [w]) length (xs ++ [v]) = length (xs ++ [w]).
Proof.
iIntros "Hlink Hτ".
iInduction xs as [|x xs'] "IH" forall (xs).
- destruct xs. 2: { done. } by iFrame.
- destruct xs as [|x xs']. { done. }
simpl.
iDestruct "Hlink" as "[t Hlink]".
iDestruct ("IH" $! xs' with "Hlink Hτ") as "[Hlink ->]".
by iFrame.
Qed.
Definition invariant γ τi hd sHd lock: iProp Σ :=
( hd ' xs xs,
hd = Loc hd isMSQueue τi hd xs
hd = Loc hd isMSQueue γ τi hd xs
sHd = Loc ' isCGQueue ' xs
lock ↦ₛ (#v false)
xsLink τi xs xs
......@@ -160,6 +213,114 @@ Section Queue_refinement.
iModIntro. iFrame.
Qed.
Definition inner x xs := (App
(Rec
(Case (ids 1)
(Fold
(InjR
(Pair (of_val x).[ren (+3)] (Fold (InjL Unit)))))
(Fold
(InjR
(Pair (Fst (ids 0))
(App (ids 1) (Unfold (Snd (ids 0)))))))))
(Unfold (of_val (isCGQueue_go xs)))).
Lemma steps_CG_enqueue_body E j K x xs :
nclose specN E
spec_ctx j fill K (inner x xs)
|={E}=> j fill K (of_val (isCGQueue_go (xs ++ [x]))).
Proof.
iIntros (HNE) "(#spec & Hj)".
iInduction xs as [|x' xs'] "IH" forall (K).
- rewrite /inner. simpl.
iMod (do_step_pure _ _ (AppRCtx (RecV _) :: K) with "[$Hj]") as "Hj"; eauto.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl.
iModIntro. iFrame.
- rewrite /inner. simpl.
iMod (do_step_pure _ _ (AppRCtx (RecV _) :: K) with "[$Hj]") as "Hj"; eauto.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl.
iMod (do_step_pure _ _ (PairLCtx _ :: InjRCtx :: FoldCtx :: K) with "[$Hj]") as "Hj"; eauto.
simpl.
iMod (do_step_pure _ _ (UnfoldCtx :: AppRCtx (RecV _) :: PairRCtx _ :: InjRCtx :: FoldCtx :: K) with "[$Hj]") as "Hj"; eauto.
simpl.
iMod ("IH" $! (PairRCtx _ :: InjRCtx :: FoldCtx :: K) with "[$Hj]") as "Hj"; eauto.
Qed.
Lemma steps_CG_enqueue E j K x xs lock :
nclose specN E
spec_ctx j fill K (App (CG_enqueue (Loc ) (Loc lock)) (of_val x))
isCGQueue (xs)
lock ↦ₛ (#v false)
|={E}=> j fill K (Unit)
isCGQueue (xs ++ [x])
lock ↦ₛ (#v false).
Proof.
iIntros (HNE) "(#spec & Hj & isQueue & lofal)".
iMod (steps_with_lock _ _ _ _ _ (isCGQueue _ _)
_ UnitV x
with "[$Hj $isQueue $lofal]") as "Hj"; eauto.
iIntros (K') "(#Hspec & isQueue & Hj)".
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl.
rewrite /isCGQueue.
iMod (step_load _ _ (UnfoldCtx :: AppRCtx (RecV _) :: StoreRCtx (LocV _) :: K') with "[Hj $isQueue]")
as "[Hj isQueue]"; eauto.
simpl.
iMod (steps_CG_enqueue_body _ j (StoreRCtx (LocV _) :: K') with "[$Hj]") as "Hj"; eauto.
iMod (step_store _ j K' with "[$Hj isQueue]") as "[Hj Hx]"; eauto.
{ rewrite /= !to_of_val //. }
iModIntro. iFrame.
Qed.
(* If you have the token and the nodeList and a cas*)
Lemma enqueue_cas E γ xs x 2 hdPt nil tail node :
{{{
nil ↦ᵢ FoldV (InjLV UnitV)
tail ↦ᵢ (LocV nil) (* ℓtail points to the nil node *)
node ↦ᵢ (FoldV (InjRV (PairV (InjRV x) (LocV tail)))) (* node contains x and points to nil *)
isNodeList γ hdPt xs
↦ᵢ{1/2} (LocV 2)
own γ ( ) (* you have the token. *)
}}}
CAS (Loc ) (Loc 2) (Loc node) @ E
{{{ RET (BoolV true);
nil ↦ᵢ{1/2} FoldV (InjLV UnitV)
tail ↦ᵢ{1/2} (LocV nil)
node ↦ᵢ{1/2} (FoldV (InjRV (PairV (InjRV x) (LocV tail))))
isNodeList γ hdPt (xs ++ [x])
own γ ( tail)
↦ᵢ{1/2} (LocV node)
}}}.
Proof.
iIntros (ϕ) "(nilPts & tailPts & nodePts & nodeList & ℓPts & tok) Hϕ".
iInduction xs as [|x' xs'] "IH" forall (hdPt).
- iDestruct "nilPts" as "[nilPts nilPts']".
iDestruct "tailPts" as "[tailPts tailPts']".
iDestruct "nodePts" as "[nodePts nodePts']".
iDestruct "nodeList" as (0 q) ">(ℓ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 %]".
inversion_clear H2.
rewrite Qp_half_half.
iMod (fracAgree_update with "tok tok'") as "[tok tok']".
iApply (wp_cas_suc with "ℓpts").
iNext. iIntros "[ℓpts ℓpts']".
iApply "Hϕ". iFrame. simpl.
iExists _, _, _. iFrame.
iExists _, _. iFrame "tailPts". iFrame.
- simpl.
iDestruct "nodeList" as (0 next q) "(FOO & BAR & nodeListTail)".
iApply ("IH" with "nilPts tailPts nodePts nodeListTail ℓPts tok").
iNext. iIntros "(nilPts & tailPts & nodePts & nodeListTail & ℓPts & tok)".
iApply "Hϕ".
iFrame.
iExists _, _, _. iFrame.
Qed.
Lemma MS_CG_counter_refinement :
[] MS_queue log CG_queue :
(TForall (TProd
......@@ -202,19 +363,20 @@ Section Queue_refinement.
iApply wp_alloc; first done. iNext.
iIntros (head) "headPts /=".
iApply wp_pure_step_later; auto. iNext.
iMod (inv_alloc nodeN _ (nodeInv (LocV tail)) with "[tailPts nilPts]") as "#nodeInv".
{ iNext. rewrite nodeInv_unfold. iExists _, _, _. iSplit; auto. iLeft. iFrame. }
iMod (inv_alloc queueN _ (invariant τi (Loc head) (Loc list) _)
with "[headPts lockPts listPts' sentinelPts tailPts' nilPts']")
iMod (own_alloc (1%Qp, to_agree tail)) as (γ) "[token1 token2]"; first done.
iMod (inv_alloc nodeN _ (nodeInv γ tail) with "[tailPts nilPts token1]") as "#nodeInv".
{ iNext. rewrite nodeInv_unfold. iExists _, _. iLeft. iFrame. }
iMod (inv_alloc queueN _ (invariant γ τi (Loc head) (Loc list) _)
with "[headPts lockPts listPts' sentinelPts tailPts' nilPts' token2]")
as "#Hinv".
{ iNext. iExists _, _, [], [].
simpl.
iFrame.
iSplit. done.
iSplitL "headPts sentinelPts tailPts' nilPts'".
{ rewrite /isMSQueue. iExists _, _, _, _, _. simpl. iFrame.
iSplitL "headPts sentinelPts tailPts' nilPts' token2".
{ rewrite /isMSQueue. iExists _, _, _, _. simpl. iFrame.
iSplitL "tailPts' nilPts'".
{ iExists _. iFrame. }
{ iExists _, _. iFrame. }
iAssumption.
}
iSplit; done.
......@@ -236,7 +398,7 @@ Section Queue_refinement.
iApply (wp_bind (fill [LetInCtx _])).
iInv queueN as (q ' xs xs) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
rewrite /isMSQueue.
iDestruct "isMSQ" as (sentinel v hdPt q p)
iDestruct "isMSQ" as (sentinel v hdPt q)
"(qPts & [sentinelPts sentinelPts'] & nodeList & nodeinv)".
iApply (wp_load with "qPts"). iNext. iIntros "qPts".
iDestruct (splitIsNodeList with "nodeList") as "[nodeList first]".
......@@ -245,7 +407,7 @@ Section Queue_refinement.
iFrame.
iSplit; auto.
iSplitL "qPts sentinelPts' nodeList nodeinv".
{ iExists _, _, _, _, _. iFrame. }
{ iExists _, _, _, _. iFrame. }
iSplit; auto.
}
simpl.
......@@ -289,12 +451,11 @@ Section Queue_refinement.
(* iApply wp_value. *)
admit.
(* xs is not the empty list *)
+ iDestruct "first" as (hd next) "(hdPts & hdPts' & Hnodes)".
+ iDestruct "first" as (hd next q0) "(hdPts & hdPts' & Hnodes)".
iApply (wp_load with "[$hdPts]"). iNext. iIntros "hdPts".
simpl.
destruct xs as [|x xs'].
{ inversion H3. }
(* iDestruct "first" as (ℓhd' ℓtail') "(hdPts' & tailPts' & Hnodes')". *)
iApply (wp_load with "[$hdPts']"). iNext. iIntros "hdPts'".
simpl.
iApply wp_pure_step_later; auto. iNext.
......@@ -311,7 +472,7 @@ Section Queue_refinement.
rename q into q'.
iInv queueN as (q '2 xs2 xs2) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
rewrite /isMSQueue.
iDestruct "isMSQ" as (sentinel2 v2 hdPt2 q2 p2)
iDestruct "isMSQ" as (sentinel2 v2 hdPt2 q2)
"(qPts & sentinelPts' & nodeList & #nodeInv')".
destruct (decide (sentinel2 = sentinel)) as [|Hneq]; subst.
* (* The queue still points to the same sentinel that we read earlier--the CAS succeeds *)
......@@ -328,12 +489,11 @@ Section Queue_refinement.
(* TODO: Maybe we could clear nodeInv at an earlier point? *)
iClear (nil) "nodeInv".
rewrite nodeInv_unfold.
iInv nodeN as (other hdPt'2 q3) "(>% & Disj)" "closeNodeInv".
{ admit. } (* FIXME *)
inversion H5 as [Heq].
iInv nodeN as (other q3) "Disj" "closeNodeInv".
(* inversion H4 as [Heq].
rewrite -Heq.
clear other H5 Heq.
iDestruct "Disj" as "[[hdPts'' hdPts''']|Right]".
clear ℓother H4 Heq. *)
iDestruct "Disj" as "[(hdPts'' & hdPts''' & tok)|Right]".
{
iDestruct (mapsto_agree with "hdPts hdPts''") as ">%".
inversion H5 as [Eq]. rewrite -Eq.
......@@ -342,21 +502,20 @@ Section Queue_refinement.
}
iDestruct "Right" as (x0 tail0) "([hdPts3 hdPts3'] & [what3 what3'] & #tailInv)".
iMod ("closeNodeInv" with "[hdPts3' what3']").
{ iNext. iExists _, _, _.
iSplit; auto.
{ iNext. iExists _, _.
iRight. iExists _, _. iFrame. iAssumption.
}
(* 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) "[ℓhdPts ℓ2Pts]".
{ iDestruct "nodeList" as (2 q1) "(ℓhdPts & ℓ2Pts & tok)".
iDestruct (mapsto_agree with "ℓhdPts hdPts") as %[= ->].
iDestruct (mapsto_agree with "hdPts' ℓ2Pts") as %[=].
}
destruct xs2 as [|x2' xs2']; simpl.
{ inversion H4. }
iDestruct "nodeList" as (tail next) "(hdPts'' & tailPts & nodeList)".
iDestruct "nodeList" as (tail next q1) "(hdPts'' & tailPts & nodeList)".
iDestruct (mapsto_agree with "hdPts hdPts''") as %[= <-].
iDestruct (mapsto_agree with "hdPts' tailPts") as %[= <- <-].
(* iAssert (⌜x = x2'⌝)%I as %<-.
......@@ -375,7 +534,7 @@ Section Queue_refinement.
iFrame.
iSplit; auto.
iSplitL "qPts hdPts'' nodeList tailPts".
{ iExists _ ,_, _, _, _. iFrame. iAssumption. }
{ iExists _ ,_, _, _. iFrame. iAssumption. }
iSplit; auto.
}
(* Step over the remainder of the code. *)
......@@ -424,7 +583,7 @@ Section Queue_refinement.
simpl.
iInv queueN as (q ' xs xs) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
rewrite /isMSQueue.
iDestruct "isMSQ" as (sentinel v hdPt q p)
iDestruct "isMSQ" as (sentinel v hdPt q)
"(qPts & [sentinelPts sentinelPts'] & nodeList & #nodeInv)".
iApply (wp_load with "qPts").
iNext. iIntros "qPts".
......@@ -433,7 +592,7 @@ Section Queue_refinement.
iFrame.
iSplit; auto.
iSplitL "qPts sentinelPts' nodeList".
{ iExists _, _, _, _, _. iFrame. iAssumption. }
{ iExists _, _, _, _. iFrame. iAssumption. }
iSplit; auto.
}
iModIntro.
......@@ -446,19 +605,20 @@ Section Queue_refinement.
iApply wp_value.
iApply wp_pure_step_later; auto. iNext.
iApply wp_value.
simpl.
(* We are now done evaluating the argument. *)
iLöb as "Hlat" forall (hdPt sentinel v q) "nodeInv".
iApply wp_pure_step_later; auto. iNext. asimpl.
iApply (wp_bind (fill [LetInCtx _])).
rewrite nodeInv_unfold.
iInv nodeN as ( 2 q0) "(>% & Disj)" "closeNodeInv".
inversion_clear H4.
iInv nodeN as (2 q0) "Disj" "closeNodeInv".
(* Are we at the end yet? *)
iDestruct "Disj" as "[(ℓPts & [ℓ2Pts ℓ2Pts'])|RIGHT]".
iDestruct "Disj" as "[(ℓPts & [ℓ2Pts ℓ2Pts'] & tok)|RIGHT]".
+ (* We are at the end and can attempt inserting our node. *)
iApply (wp_load with "ℓPts").
iNext. iIntros "ℓPts". simpl.
iMod ("closeNodeInv" with "[ℓPts ℓ2Pts']") as "_".
{ iNext. iExists _, _, _. iSplit; auto. iLeft. iFrame. }
iMod ("closeNodeInv" with "[ℓPts ℓ2Pts' tok]") as "_".
{ iNext. iExists _, _. auto. iLeft. iFrame. }
iModIntro.
iApply wp_pure_step_later; auto. iNext.
iApply (wp_bind (fill [CaseCtx _ _])).
......@@ -475,32 +635,109 @@ Section Queue_refinement.
somehow extract that ℓ is the last node. *)
iInv queueN as (q2 '2 xs xs) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
rewrite /isMSQueue.
iDestruct "isMSQ" as (sentinel2 v3 hdPt q2 p2)
iDestruct "isMSQ" as (sentinel2 v3 hdPt' q2)
"(qPts & sentinelPts2 & nodeList & nodeinv)".
iInv nodeN as (tup 2' q0') "(>% & Disj)" "closeNodeInv".
{ admit. }
inversion H2. rewrite -H4. clear H2 H4.
iInv nodeN as (2' q0') "Disj" "closeNodeInv".
destruct (decide (2' = 2)) as [|Hneq]; subst.
* (* We are still at the end. *)
iDestruct "Disj" as "[(ℓPts & ℓ2Pts2)|Right]".
iDestruct "Disj" as "[(>ℓPts & >ℓ2Pts2 & >tok)|Right]".
(* 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 (x next) "(ℓPts' & ℓ2Pts' & nodeInvFunk)".
iDestruct (mapsto_agree with "ℓ2Pts ℓ2Pts'") as ">%".
inversion H2.
inversion H3.
}
simpl.
clear.
destruct xs as [|x xs'].
-- simpl.
iDestruct "nodeList" as (0) "(ℓhdPt & ℓ0Pts)".
(* FIXME: We need to be able to conclude that ℓhdPt is equal to ℓ. *)
admit.
-- admit.
* admit. (* Another thread changed the end in the meantime. *)
+ admit. (* Gotta keep on going. *)
iApply (enqueue_cas with "[$nilPts $tailPts $nodePts $nodeList $ℓPts $tok]").
iNext. iIntros "(nilPts & tailPts & nodePts & nodeList & tok & ℓPts)".
iMod (inv_alloc nodeN _ (nodeInv γ tail) with "[tailPts nilPts tok]") as "#nodeInvTail".
{ iNext.
rewrite nodeInv_unfold.
iExists _, _. iLeft. iFrame.
}
iMod (steps_CG_enqueue with "[$Hspec $Hj $lofal $Hsq]") as "(Hj & Hsq & lofal)".
{ solve_ndisj. }
iMod ("closeNodeInv" with "[nodePts ℓPts]").
{ iNext. iExists _, _. iRight. iExists _, _. iFrame. iAssumption. }
iModIntro.
iMod ("Hclose" with "[qPts lofal Hlink Hsq sentinelPts2 nodeList nodeinv]") as "_".
{ iNext. iExists _, _, (xs ++ [v1]), (xs ++ [v2]).
iFrame.
iSplit; auto.
iSplitL "qPts sentinelPts2 nodeList nodeinv".
{ iExists _, _, _, _. iFrame. }
iSplit; auto.