Commit 62a67970 authored by Simon Friis Vindum's avatar Simon Friis Vindum

Use fractional points-to predicates, fix nodeInv, and more

parent 7603e66d
......@@ -17,20 +17,21 @@ Section Queue_refinement.
Definition noneV := InjLV UnitV.
Definition someV v := InjRV v.
(* Definition nodeInv_pre : valO -n> (iPropO Σ) := λne nodeInv v, *)
(* (∃ ℓ m v ℓtail, *)
(* ⌜n = Loc ℓ⌝ ∗ ℓ ↦ᵢ (FoldV v) *)
(* ∗ (⌜v = noneV⌝ *)
(* ∨ (∃ n', ⌜v = someV (PairV v (Loc ℓtail))⌝ *)
(* ∗ ℓtail ↦ᵢ n' *)
(* ∗ ▷(nodeInv n')) *)
(* ))%I. *)
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 v (LocV tail)) tail ↦ᵢ n' (P n'))
))%I.
Solve Obligations with solve_proper.
(* Global Instance nodeInv_pre_contractive Q : Contractive (nodeInv_pre Q). *)
Global Instance nodeInv_pre_contractive : Contractive (nodeInv_pre).
(* Proof. solve_contractive. Qed. *)
Proof. solve_contractive. Qed.
(* Definition StackLink (Q : D) : D := fixpoint (StackLink_pre Q). *)
Definition nodeInv : valO -n> iPropO Σ := fixpoint (nodeInv_pre).
Definition isStackList ( : loc) (xs : list val) : iProp Σ :=
match xs with
......@@ -38,34 +39,51 @@ Section Queue_refinement.
| x :: xs' => True (* FIXME *)
end.
Fixpoint isNodeList ( : loc) (xs : list val) : iProp Σ :=
(* 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 Σ :=
match xs with
| nil => ↦ᵢ FoldV noneV
| x :: xs' =>
( tail next,
↦ᵢ FoldV (someV (PairV x (LocV tail)))
tail ↦ᵢ (LocV next)
isNodeList next xs')
↦ᵢ{q} FoldV (someV (PairV x (LocV tail)))
tail ↦ᵢ{q} (LocV next)
isNodeList q next xs')
end.
Definition sentinelInv sentinel xs v hdPt hd : iProp Σ :=
sentinel ↦ᵢ (FoldV (someV (PairV v (LocV hdPt))))
hdPt ↦ᵢ (LocV hd)
isNodeList hd xs.
(* Represents that the location ℓ points to a series of nodes corresponding to
the list `xs` _and potentially more nodes_. The difference between this and
isStackList is that this predicates does not say exactly what the end, i.e.
the final node, is because this may change. *)
Fixpoint firstXsValues q ( : 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' =>
( tail next,
↦ᵢ{q} FoldV (someV (PairV x (LocV tail)))
tail ↦ᵢ{q} (LocV next)
firstXsValues q next xs')
end.
Lemma splitIsNodeList q xs : isNodeList q xs - isNodeList (q/2) xs firstXsValues (q/2) xs : iProp Σ.
Proof.
iIntros "isNodeList".
(* generalize dependent ℓ. *)
iInduction xs as [|x xs'] "IH" forall (); simpl.
- iFrame.
- iDestruct "isNodeList" as (tail next) "([ℓPts1 ℓPts2] & [ℓtailPts1 ℓtailPts2] & Hnl)".
iDestruct ("IH" with "Hnl") as "[Ha Hb]".
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,
(* ∃ ℓsentinel ℓfirst ℓhead, *)
(* ℓ points to the sentinel *)
( sentinel v hdPt hd q p,
↦ᵢ (LocV sentinel)
( v hdPt hd n, inv n (sentinelInv sentinel xs v hdPt hd))
(* The sentinel points to the first actual element *)
(* ∗ ℓsentinel ↦ᵢ{1/2} (FoldV (someV (PairV noneV (LocV ℓfirst)))) *)
(* ∗ ℓfirst ↦ᵢ (LocV ℓhead) *)
(* ∗ isNodeList ℓhead xsᵢ *)
)%I.
sentinel ↦ᵢ{q} (FoldV (someV (PairV v (LocV hdPt))))
hdPt ↦ᵢ{q} (LocV hd)
isNodeList p hd xs)%I.
(* Definition isStackList (τi : D) (ℓ : loc) (xs : list val) (xs' : list val) : iProp Σ := *)
(* (⌜True⌝)%I. *)
......@@ -128,23 +146,15 @@ Section Queue_refinement.
iApply wp_alloc; first done. iNext.
iIntros (head) "headPts /=".
iApply wp_pure_step_later; auto. iNext.
iMod (inv_alloc (queueN.@"S") _ (sentinelInv sentinel [] noneV tail nil)
with "[sentinelPts tailPts nilPts]")
as "#sentinelI".
{ iNext. iFrame. }
iMod (inv_alloc queueN _ (invariant τi (Loc head) (Loc list) _)
with "[headPts lockPts listPts']")
with "[headPts lockPts listPts' sentinelPts tailPts nilPts]")
as "#Hinv".
{ iNext. iExists _, _, [], [].
simpl.
iFrame.
iSplit. done.
iSplitL "headPts".
{ iExists _.
iFrame.
iExists _, _, _, _.
iAssumption.
}
iSplitL "headPts sentinelPts tailPts nilPts".
{ iExists _, _, _, _, _, _. iFrame. }
iSplit; done.
}
iApply wp_value.
......@@ -162,16 +172,17 @@ Section Queue_refinement.
rewrite with_lock_of_val.
iApply wp_pure_step_later; auto. iNext. asimpl.
iApply (wp_bind (fill [LetInCtx _])).
iInv queueN as (hd ' xs xs') "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
iDestruct "isMSQ" as (sentinel) "[hdPts #Hsentinel]".
iApply (wp_load with "hdPts").
iNext. iIntros "hdPts".
iMod ("Hclose" with "[hdPts lofal Hlink Hsq]").
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".
iDestruct (splitIsNodeList with "isNodeList") as "[isNodeList Hnodes]".
iMod ("Hclose" with "[qPts lofal Hlink Hsq sentinelPts' hdPts' isNodeList]") as "_".
{ iNext. iExists _, _, _, _.
iFrame.
iSplit; auto.
iSplitL "hdPts".
{ iExists _. iFrame. iAssumption. }
iSplitL "qPts sentinelPts' hdPts' isNodeList".
{ iExists _, _, _, _, _, _. iFrame. }
iSplit; auto.
}
simpl.
......@@ -179,12 +190,9 @@ Section Queue_refinement.
iApply wp_pure_step_later; auto. iNext. asimpl.
iApply (wp_bind (fill [LetInCtx _])).
iApply (wp_bind (fill [UnfoldCtx; CaseCtx _ _])).
iDestruct "Hsentinel" as (v l1 l2 n) "Hsentinv".
iInv n as "[sentinelPts HRest]" "Hclose".
iApply (wp_load with "sentinelPts").
iNext. iIntros "sentinelPts".
iMod ("Hclose" with "[$]") as "_".
iModIntro. simpl.
simpl.
iApply (wp_bind (fill [CaseCtx _ _])).
iApply wp_pure_step_later; auto. iNext.
iApply wp_value.
......@@ -200,34 +208,42 @@ Section Queue_refinement.
iApply (wp_bind (fill [LoadCtx])).
iApply wp_pure_step_later; auto. iNext.
iApply wp_value. simpl.
iInv n as "(sentinelPts & l2Pts & HRest)" "Hclose".
iApply (wp_load with "[$]").
iNext. iIntros "l2Pts".
iMod ("Hclose" with "[$]") as "_".
iModIntro.
iApply (wp_load with "[$hdPts]"). iNext. iIntros "hdPts".
simpl.
iInv n as "(sentinelPts & l2Pts & Hnode)" "Hclose".
destruct xs as [|x xs''].
+ (* xs is the empty list *)
assert (xs' = []) as ->. { destruct xs'. done. inversion H3. }
destruct xs as [|x xs'']; simpl.
(* xs is the empty list *)
+ assert (xs' = []) as ->.
{ destruct xs'. done. inversion H3. }
simpl.
iApply (wp_load with "[$]").
iNext. iIntros "Hnode".
iMod ("Hclose" with "[$]") as "_".
iModIntro.
iInv queueN as (hd ' xs xs') "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
iApply wp_pure_step_later; auto. simpl. iNext.
iApply wp_value.
iApply wp_pure_step_later; auto. iNext. simpl.
(* FIXME: Hnodes should tell us something useful in this case. *)
(* iApply (wp_load with "[$]"). *)
(* iNext. iIntros "Hnode". *)
(* iMod ("Hclose" with "[sentinelPts' l1pts' Hnode]") as "_". *)
(* { iExists _, _. iFrame. } *)
(* iModIntro. *)
(* iInv queueN as (ℓhd ℓ' xs xs') "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose". *)
(* iApply wp_pure_step_later; auto. simpl. iNext. *)
(* iApply wp_value. *)
(* iApply wp_pure_step_later; auto. iNext. simpl. *)
(* iApply wp_value. *)
admit.
(* xs is not the empty list *)
+ iDestruct "Hnodes" as (hd' tail') "(hdPts' & tailPts' & Hnodes')".
iApply (wp_load with "[$hdPts']"). iNext. iIntros "hdPts'".
simpl.
iApply wp_pure_step_later; auto. iNext.
iApply wp_value.
+ (* xs is not the empty list *)
iApply (wp_load with "[$]").
iNext. iIntros "l2Pts".
iMod ("Hclose" with "[$]") as "_".
iModIntro.
simpl.
admit.
iApply wp_pure_step_later; auto. iNext.
iApply (wp_bind (fill [IfCtx _ _])).
asimpl.
iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _)])).
iApply (wp_bind (fill [LoadCtx])).
iApply wp_pure_step_later; auto. iNext.
iApply wp_value. simpl.
iApply (wp_load with "hdPts"). iNext. iIntros "hdPts".
simpl.
(* FIXME: Here we must open the queue invariant again. *)
admit.
- (* enqueue *)
iIntros ([v1 v2]) "!> #Hrel".
clear j K.
......@@ -235,18 +251,4 @@ Section Queue_refinement.
rewrite with_lock_of_val.
Abort.
Lemma steps_CG_locked_pop_suc E j K st v w l :
nclose specN E
spec_ctx st ↦ₛ FoldV (InjRV (PairV w v)) l ↦ₛ (#v false)
j fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
|={E}=> j fill K (InjR (of_val w)) st ↦ₛ v l ↦ₛ (#v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ FoldV (InjRV (PairV w v)))%I
_ (InjRV w) UnitV
with "[$Hj $Hx $Hl]") as "Hj"; eauto.
iIntros (K') "[#Hspec Hxj]".
iApply steps_CG_pop_suc; eauto.
Qed.
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