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

Advance dequeue proof when queue is non-empty

parent 62a67970
......@@ -172,7 +172,7 @@ Section Queue_refinement.
rewrite with_lock_of_val.
iApply wp_pure_step_later; auto. iNext. asimpl.
iApply (wp_bind (fill [LetInCtx _])).
iInv queueN as (q ' xs xs') "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
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)".
iApply (wp_load with "qPts"). iNext. iIntros "qPts".
......@@ -210,10 +210,10 @@ Section Queue_refinement.
iApply wp_value. simpl.
iApply (wp_load with "[$hdPts]"). iNext. iIntros "hdPts".
simpl.
destruct xs as [|x xs'']; simpl.
destruct xs as [|x xs']; simpl.
(* xs is the empty list *)
+ assert (xs' = []) as ->.
{ destruct xs'. done. inversion H3. }
+ assert (xs = []) as ->.
{ destruct xs. done. inversion H3. }
simpl.
(* FIXME: Hnodes should tell us something useful in this case. *)
(* iApply (wp_load with "[$]"). *)
......@@ -228,7 +228,9 @@ Section Queue_refinement.
(* iApply wp_value. *)
admit.
(* xs is not the empty list *)
+ iDestruct "Hnodes" as (hd' tail') "(hdPts' & tailPts' & Hnodes')".
+ destruct xs as [|x xs'].
{ inversion H3. }
iDestruct "Hnodes" as (hd' tail') "(hdPts' & tailPts' & Hnodes')".
iApply (wp_load with "[$hdPts']"). iNext. iIntros "hdPts'".
simpl.
iApply wp_pure_step_later; auto. iNext.
......@@ -242,8 +244,48 @@ Section Queue_refinement.
iApply wp_value. simpl.
iApply (wp_load with "hdPts"). iNext. iIntros "hdPts".
simpl.
(* FIXME: Here we must open the queue invariant again. *)
admit.
rename q into q'.
iInv queueN as (q '2 xs2 xs'2) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
(* clear. *)
iDestruct "isMSQ" as (sentinel2 v2 hdPt2 hd2 q2 p2)
"(qPts & sentinelPts' & hdPts2 & isNodeList)".
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.
iNext. iIntros "qPts".
(* We have opened the queue invariant twice. Since the queue pointer
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. *)
iAssert (v = v2)%I as %<-.
{ iDestruct (mapsto_agree with "sentinelPts sentinelPts'") as %[=->]. done. }
iAssert (⌜ℓhdPt = hdPt2)%I as %<-.
{ 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. *)
destruct xs2 as [|x2' xs2']; simpl.
{ iDestruct (mapsto_agree with "isNodeList hdPts'") as %[=->]. }
iDestruct "isNodeList" as (tail next) "[hdPts'' isNodeList']".
iAssert (x = x2')%I as %<-.
{ iDestruct (mapsto_agree with "hdPts' hdPts''") as %[=<-]. done. }
(* We must now reestablish the invariant. *)
iMod ("Hclose" with "[qPts lofal Hlink Hsq isNodeList']") as "_".
{ iNext.
rewrite /invariant.
iExists _, _, xs', xs'.
iFrame.
iSplit; auto.
iSplit; auto.
rewrite /isMSQueue.
iExists _, _, _ ,_, _, _.
iFrame.
}
*
iApply (wp_load with "qPts"). iNext. iIntros "qPts".
admit.
- (* enqueue *)
iIntros ([v1 v2]) "!> #Hrel".
clear j K.
......
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