Commit 38510705 authored by Simon Friis Vindum's avatar Simon Friis Vindum

Advance enqueue proof, include node invariant in queue invariant

parent 07bd8590
......@@ -7,7 +7,8 @@ From iris_examples.logrel.F_mu_ref_conc.examples.queue Require Import
CG_queue MS_queue.
From iris.proofmode Require Import tactics.
Definition queueN : namespace := nroot .@ "stack".
Definition queueN : namespace := nroot .@ "queue".
Definition nodeN : namespace := queueN .@ "node".
Section Queue_refinement.
Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}.
......@@ -19,12 +20,13 @@ Section Queue_refinement.
Program Definition nodeInv_pre : (valO -n> iPropO Σ) -n> (valO -n> iPropO Σ) :=
λne P n,
( v q,
n = LocV ℓ⌝ ↦ᵢ{q} (FoldV v)
(v = noneV
( (n' : valO) tail,
v = someV (PairV (InjRV v) (LocV tail)) tail ↦ᵢ n' (P n'))
))%I.
( , n = LocV ℓ⌝
( ↦ᵢ{1/2} FoldV noneV (* FIXME: Maybe we need more info here? *)
( (x : valO) q tail n',
↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV tail)))
tail ↦ᵢ{q} n' inv nodeN (P n')
)))%I.
Solve Obligations with solve_proper.
Global Instance nodeInv_pre_contractive : Contractive (nodeInv_pre).
......@@ -33,6 +35,15 @@ Section Queue_refinement.
Definition nodeInv : valO -n> iPropO Σ := fixpoint (nodeInv_pre).
Lemma nodeInv_unfold n :
nodeInv n ( , n = LocV ℓ⌝
( ↦ᵢ{1/2} FoldV noneV
( (x : valO) q tail n',
↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV tail)))
tail ↦ᵢ{q} n' inv nodeN (nodeInv n')
)))%I.
Proof. rewrite /nodeInv. apply (fixpoint_unfold nodeInv_pre n). Qed.
Fixpoint isCGQueue_go (xs : list val) : val :=
match xs with
| nil => FoldV noneV
......@@ -47,7 +58,7 @@ Section Queue_refinement.
*)
Fixpoint isNodeList q ( : loc) (xs : list val) : iProp Σ :=
match xs with
| nil => ↦ᵢ FoldV noneV
| nil => ↦ᵢ{1/2} FoldV noneV
| x :: xs' =>
( tail next,
↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV tail)))
......@@ -70,6 +81,16 @@ Section Queue_refinement.
firstXsValues q next xs')
end.
Lemma firstXsValues_split q xs : firstXsValues q xs - firstXsValues (q/2) xs firstXsValues (q/2) 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 ("IH" with "Hnl") as "[Ha Hb]".
iSplitL "ℓPts1 ℓtailPts1 Ha"; iExists _, _; iFrame.
Qed.
Lemma splitIsNodeList q xs : isNodeList q xs - isNodeList (q/2) xs firstXsValues (q/2) xs : iProp Σ.
Proof.
iIntros "isNodeList".
......@@ -87,10 +108,10 @@ Section Queue_refinement.
↦ᵢ (LocV sentinel)
sentinel ↦ᵢ{q} (FoldV (someV (PairV v (LocV hdPt))))
hdPt ↦ᵢ{q} (LocV hd)
isNodeList p hd xs)%I.
(* Definition isCGQueue (τi : D) (ℓ : loc) (xs : list val) (xs' : list val) : iProp Σ := *)
(* (⌜True⌝)%I. *)
isNodeList p hd xs
(* ∗ firstXsValues p ℓhd xsᵢ *)
inv nodeN (nodeInv (LocV hd))
)%I.
Fixpoint xsLink (τi : D) (xs xs : list val) : iProp Σ :=
match (xs, xs) with
......@@ -174,7 +195,7 @@ Section Queue_refinement.
iApply (wp_bind (fill [PairRCtx (InjLV UnitV); InjRCtx; FoldCtx])).
iApply (wp_bind (fill [AllocCtx])).
iApply wp_alloc; first done.
iNext. iIntros (nil) "nilPts /=".
iNext. iIntros (nil) "[nilPts1 nilPts2] /=".
iApply wp_alloc; first done.
iNext. iIntros (tail) "tailPts /=".
iApply wp_value.
......@@ -183,15 +204,17 @@ 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 nil)) with "[nilPts1]") as "#nodeInv".
{ iNext. rewrite nodeInv_unfold. iExists _. auto. }
iMod (inv_alloc queueN _ (invariant τi (Loc head) (Loc list) _)
with "[headPts lockPts listPts' sentinelPts tailPts nilPts]")
with "[headPts lockPts listPts' sentinelPts tailPts nilPts2]")
as "#Hinv".
{ iNext. iExists _, _, [], [].
simpl.
iFrame.
iSplit. done.
iSplitL "headPts sentinelPts tailPts nilPts".
{ iExists _, _, _, _, _, _. iFrame. }
iSplitL "headPts sentinelPts tailPts nilPts2".
{ iExists _, _, _, _, _, _. iFrame. iAssumption. }
iSplit; done.
}
iApply wp_value.
......@@ -211,14 +234,14 @@ Section Queue_refinement.
iApply (wp_bind (fill [LetInCtx _])).
iInv queueN as (q ' xs xs) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
iDestruct "isMSQ" as (sentinel v hdPt hd q p)
"(qPts & [sentinelPts sentinelPts'] & [hdPts hdPts'] & isNodeList)".
"(qPts & [sentinelPts sentinelPts'] & [hdPts hdPts'] & nodeList & nodeinv)".
iApply (wp_load with "qPts"). iNext. iIntros "qPts".
iDestruct (splitIsNodeList with "isNodeList") as "[isNodeList Hnodes]".
iMod ("Hclose" with "[qPts lofal Hlink Hsq sentinelPts' hdPts' isNodeList]") as "_".
iDestruct (splitIsNodeList with "nodeList") as "[nodeList first]".
iMod ("Hclose" with "[qPts lofal Hlink Hsq sentinelPts' hdPts' nodeList nodeinv]") as "_".
{ iNext. iExists _, _, _, _.
iFrame.
iSplit; auto.
iSplitL "qPts sentinelPts' hdPts' isNodeList".
iSplitL "qPts sentinelPts' hdPts' nodeList nodeinv".
{ iExists _, _, _, _, _, _. iFrame. }
iSplit; auto.
}
......@@ -267,7 +290,7 @@ Section Queue_refinement.
(* xs is not the empty list *)
+ destruct xs as [|x xs'].
{ inversion H3. }
iDestruct "Hnodes" as (hd' tail') "(hdPts' & tailPts' & Hnodes')".
iDestruct "first" as (hd' tail') "(hdPts' & tailPts' & Hnodes')".
iApply (wp_load with "[$hdPts']"). iNext. iIntros "hdPts'".
simpl.
iApply wp_pure_step_later; auto. iNext.
......@@ -283,9 +306,8 @@ Section Queue_refinement.
simpl.
rename q into q'.
iInv queueN as (q '2 xs2 xs2) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
(* clear. *)
iDestruct "isMSQ" as (sentinel2 v2 hdPt2 hd2 q2 p2)
"(qPts & sentinelPts' & hdPts2 & isNodeList)".
"(qPts & sentinelPts' & hdPts2 & nodeList & #nodeInv')".
destruct (decide (sentinel2 = sentinel)) as [|Hneq]; subst.
* (* The queue still points to the same sentinel that we read earlier--the CAS succeeds *)
iApply (wp_cas_suc with "qPts"); auto.
......@@ -300,14 +322,31 @@ Section Queue_refinement.
{ iDestruct (mapsto_agree with "sentinelPts sentinelPts'") as %[=->]. done. }
iAssert (⌜ℓhd = hd2)%I as %<-.
{ iDestruct (mapsto_agree with "hdPts hdPts2") as %[=->]. done. }
(* xs2 is not necessarily equal to xs, but 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. *)
(* TODO: Maybe we could clear nodeInv at an earlier point? *)
iClear (nil) "nodeInv".
rewrite nodeInv_unfold.
iInv nodeN as (other) "(>% & two)" "closeNodeInv".
{ admit. } (* FIXME *)
inversion H5 as [Heq].
rewrite -Heq.
clear other H5 Heq.
iDestruct "two" as "[hdPts''|Right]".
{ iDestruct (mapsto_agree with "hdPts' hdPts''") as ">%". inversion H5. }
iDestruct "Right" as (x0 q0 tail0 nwhat) "([hdPts3 hdPts3'] & [what3 what3'] & #tailInv)".
iMod ("closeNodeInv" with "[hdPts3' what3' tailInv]").
{ iNext. iExists _. iFrame.
iSplit; auto.
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 (mapsto_agree with "isNodeList hdPts'") as %[=->]. }
{ iDestruct (mapsto_agree with "nodeList hdPts'") as %[=->]. }
destruct xs2 as [|x2' xs2']; simpl.
{ inversion H4. }
iDestruct "isNodeList" as (tail next) "[hdPts'' isNodeList]".
iDestruct "nodeList" as (tail next) "(hdPts'' & tailPts & nodeList)".
iAssert (x = x2')%I as %<-.
{ iDestruct (mapsto_agree with "hdPts' hdPts''") as %[=<-]. done. }
iDestruct "Hlink" as "[Hτi Hlink]".
......@@ -316,15 +355,17 @@ Section Queue_refinement.
{ solve_ndisj. }
(* FIXME: I think the brackets can be removed here. *)
(* We are now ready to reestablish the invariant. *)
iMod ("Hclose" with "[qPts lofal Hlink Hsq isNodeList hdPts'']") as "_".
iMod ("Hclose" with "[qPts lofal Hlink Hsq nodeList hdPts'' hdPts3 what3 tailPts tailInv]") as "_".
{ iNext.
(* We now determine that nwhat is equal to LocV ℓnext. *)
iDestruct (mapsto_agree with "hdPts3 hdPts''") as %[= -> ->].
iDestruct (mapsto_agree with "what3 tailPts") as %->.
rewrite /invariant.
iExists _, _, xs2', xs2'.
iFrame.
iSplit; auto.
iSplitL "qPts hdPts'' isNodeList".
{ iExists _, _, _ ,_, _, _.
iFrame. }
iSplitL "qPts hdPts'' nodeList tailPts".
{ iExists _, _, _ ,_, _, _. iFrame. iAssumption. }
iSplit; auto.
}
(* Step over the remainder of the code. *)
......@@ -347,10 +388,78 @@ Section Queue_refinement.
(* iApply (wp_load with "qPts"). iNext. iIntros "qPts". *)
admit.
- (* enqueue *)
iClear (j K) "nodeInv".
iIntros ([v1 v2]) "!> #Hrel".
clear j K.
iIntros (j K) "Hj". simpl.
rewrite with_lock_of_val.
iApply wp_pure_step_later; auto. iNext.
iApply (wp_bind (fill [LetInCtx _])).
asimpl.
(* Step ove the allocation and creation of the new node. *)
iApply (wp_bind (fill [PairRCtx (InjRV _); InjRCtx; FoldCtx; AllocCtx])).
iApply (wp_bind (fill [AllocCtx])).
iApply wp_alloc; first done.
iNext. iIntros (nil) "nilPts". simpl.
iApply wp_alloc; first done.
iNext. iIntros (tail) "tailPts". simpl.
iApply wp_alloc; first done.
iNext. iIntros (node) "nodePts /=".
iApply wp_pure_step_later; auto. iNext.
(* Evaluate the argument to the recursive function. *)
iApply (wp_bind (fill [AppRCtx (RecV _)])).
iApply (wp_bind (fill [SndCtx])).
iApply (wp_bind (fill [CaseCtx _ _])).
iApply (wp_bind (fill [UnfoldCtx])).
iApply (wp_bind (fill [LoadCtx])).
simpl.
iInv queueN as (q ' xs xs) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
rewrite /isMSQueue.
iDestruct "isMSQ" as (sentinel v hdPt hd q p)
"(qPts & [sentinelPts sentinelPts'] & [hdPts hdPts'] & nodeList & #nodeInv)".
iApply (wp_load with "qPts").
iNext. iIntros "qPts".
iMod ("Hclose" with "[qPts lofal Hlink Hsq sentinelPts' hdPts' nodeList nodeInv]") as "_".
{ iNext. iExists _, _, _, _.
iFrame.
iSplit; auto.
iSplitL "qPts sentinelPts' hdPts' nodeList".
{ iExists _, _, _, _, _, _. iFrame. }
iSplit; auto.
}
iModIntro.
iApply (wp_load with "sentinelPts").
iNext. iIntros "sentinelPts".
simpl.
iApply wp_pure_step_later; auto. iNext.
iApply wp_value. simpl.
iApply wp_pure_step_later; auto. iNext. simpl.
iApply wp_value.
iApply wp_pure_step_later; auto. iNext.
iApply wp_value.
(* We are now done evaluating the argument. *)
iApply wp_pure_step_later; auto. iNext. asimpl.
iApply (wp_bind (fill [LetInCtx _])).
iApply (wp_load with "hdPts").
iNext. iIntros "hdPts".
simpl.
iApply wp_pure_step_later; auto. iNext. asimpl.
iApply (wp_bind (fill [CaseCtx _ _])).
iApply (wp_bind (fill [UnfoldCtx])).
rewrite nodeInv_unfold.
iInv nodeN as (hd') "(>% & Disj)" "closeNodeInv".
inversion H4 as [eq]. rewrite -eq. clear eq.
(* Are we at the end yet? *)
iDestruct "Disj" as "[hdPts'|right]".
+ (* We are at the end and can attempt inserting our node. *)
iApply (wp_load with "hdPts'").
iNext. iIntros "hdPts'".
admit.
+ (* Gotta keep on going. *)
iDestruct "right" as (x q' tail' n') "(headPts & tailPts' & nextInv)".
(* iMod (inv_alloc nodeN _ (nodeInv (LocV nil)) with "[nilPts1]") as "#nodeInv".
{ iNext. rewrite nodeInv_unfold. iExists _. auto. } *)
iApply (wp_load with "hdPts").
iNext. iIntros "hdPts".
Abort.
End Queue_refinement.
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