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

Dequeue almost done with new approach

parent 95b1f98c
......@@ -26,14 +26,35 @@ Definition nodeDead := 2 : mnat.
Canonical Structure gnameO := leibnizO gname.
Definition mapUR : ucmraT := gmapUR loc (agreeR (leibnizO (gname * loc))).
(* Definition nodeR : ucmraT := authUR (mapUR). *)
Definition nodeUR : ucmraT := authUR (gmapUR loc (agreeR (leibnizO (gname * loc)))).
Definition one_shotR := csumR (exclR unitO) (optionR (exclR unitO)).
Definition pending : one_shotR := Cinl (Excl ()).
Definition shotNone : one_shotR := sCinr (None).
Definition shotNone : one_shotR := Cinr (None).
Definition shotSome : one_shotR := Cinr (Some (Excl ())).
Section my_map.
Context `{Monoid M o}.
Context `{Countable K} {A : Type}.
Implicit Types m : gmap K A.
Implicit Types f g : K A M.
Context {PROP : bi}.
Implicit Types Φ Ψ : K A PROP.
Context `{Monoid M o}.
Implicit Types xs : list M.
Infix "`o`" := o (at level 50, left associativity).
(* These lemmas are committed upstream and should be available from Iris at
some point (when?) *)
Lemma big_opM_insert_delete `{Countable K} {B} (f : K B M) (m : gmap K B) i x :
([^o map] ky <[i:=x]> m, f k y) f i x `o` [^o map] ky (delete i m), f k y.
Proof. Admitted.
Lemma big_sepM_insert_delete Φ m i x :
(([ map] ky <[i:=x]> m, Φ k y) Φ i x [ map] ky (delete i m), Φ k y)%I.
Proof. Admitted.
End my_map.
Section Queue_refinement.
Context `{heapIG Σ, cfgSG Σ, inG Σ fracAgreeR, inG Σ exlTokR, inG Σ nodeUR, inG Σ nodeStateR}.
......@@ -47,10 +68,7 @@ Section Queue_refinement.
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 [_ Hv].
iIntros "!%"; by apply agree_op_invL'.
iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %[_ Hv%agree_op_invL'].
Qed.
Lemma fracAgree_combine γ (q1 q2 : Qp) v1 v2 :
......@@ -76,6 +94,22 @@ Section Queue_refinement.
by apply cmra_update_exclusive.
Qed.
Lemma node_update ι (x y : mnat) : x y own ι ( x) == own ι ( y).
Proof.
iIntros. iApply (own_update with "[$]"). by eapply auth_update_auth, mnat_local_update.
Qed.
Lemma update_sentinel_dead ι : own ι ( nodeSentinel) == own ι ( nodeDead).
Proof. iApply node_update. unfold nodeSentinel, nodeDead. lia. Qed.
Lemma update_live_sentinel ι : own ι ( nodeLive) == own ι ( nodeSentinel).
Proof. iApply node_update. unfold nodeLive, nodeSentinel. lia. Qed.
Lemma state_agree ι q p s1 s2 : own ι ({q} s1) - own ι ({p} s2) - s1 = s2.
Proof.
iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %E%auth_auth_frac_op_invL.
Qed.
Program Definition nodeInv_pre γ : (locO -n> iPropO Σ) -n> (locO -n> iPropO Σ) :=
λne P ,
( 2 q,
......@@ -110,7 +144,7 @@ Section Queue_refinement.
| nil => 2 q, ↦ᵢ{1/2} (LocV 2) 2 ↦ᵢ{q} FoldV noneV own γ ( )
| x :: xs' =>
( 2 next q ι,
own κ ( {[ := to_agree (ι, next) ]})
own κ ( {[ 2 := to_agree (ι, next) ]})
own ι ({1/2} nodeLive)
↦ᵢ{q} (LocV 2) 2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV next)))
isNodeList γ κ next xs')
......@@ -143,6 +177,8 @@ Section Queue_refinement.
own γ ( (to_agree <$> m) : nodeUR)
[ map] s a m, ( ι n, a = (ι, n) sentinelInv ι q s n).
Definition node_singleton s ι n : mapUR := {[ s := to_agree (ι, n)]}.
Definition node_mapsto γ s ι (n : loc) : iProp Σ :=
own γ ( {[ s := to_agree (ι, n)]} : nodeUR).
......@@ -165,6 +201,7 @@ Section Queue_refinement.
{ apply (mapUR_alloc _ s). rewrite lookup_fmap. rewrite a. done. }
rewrite fmap_insert.
iFrame.
(* iDestruct (big_sepM_insert with "[mon sentInv]") as "HI". *)
iApply big_sepM_insert; first done.
iFrame.
iExists _, _. iFrame. done.
......@@ -173,24 +210,84 @@ Section Queue_refinement.
Lemma map_singleton_included (m : gmap loc (gname * loc)) (l : loc) v :
({[l := to_agree v]} : mapUR) ((to_agree <$> m) : mapUR) m !! l = Some v.
Proof.
rewrite singleton_included=> -[[q' av] []].
rewrite singleton_included_l=> -[[q' av] []].
(* rewrite lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]].
move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //. *)
Admitted.
Lemma node_lookup γ (ι : gname) (q s n : loc) (m : gmap loc (gname * loc)) :
Lemma auth_node_mapsto_Some γ m s ι n :
own γ ( (to_agree <$> m) : nodeUR) -
( [ map] s a m, ( ι n, a = (ι, n) sentinelInv ι q s n)) -
node_mapsto γ s ι n -
( sentinelInv ι q s n)
m !! s = Some (ι, n).
Proof.
iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %[E%map_singleton_included _]%auth_both_valid.
Qed.
Lemma node_mapsto_agree γ s ι ι' n n' :
node_mapsto γ s ι n -
node_mapsto γ s ι' n' -
⌜ι = ι' ⌜ℓn = n'.
Proof.
(* FIXME: Why is this so painful? *)
iIntros "a b".
unfold node_mapsto.
iDestruct (own_valid_2 with "a b") as %Hv.
rewrite -auth_frag_op in Hv.
apply (auth_frag_valid ({[ _ := _]} {[ _ := _]})) in Hv.
rewrite op_singleton in Hv.
apply singleton_valid in Hv.
apply (@agree_op_invL' (leibnizO (gname * loc)) _ (ι, n) (ι', n')) in Hv.
inversion Hv.
done.
Qed.
(* Reinsert a node that has been taken out. *)
Lemma reinsert_node_subset q s ι n (m : gmap loc (gname * loc)) :
m !! s = Some (ι, n)
([ map] s a (delete s m), ( ι n', a = (ι, n') sentinelInv ι q s n')) -
sentinelInv ι q s n
-
([ map] s a m, ( ι n', a = (ι, n') sentinelInv ι q s n')).
Proof.
iIntros (eq) "mon new".
iDestruct (big_sepM_insert_delete with "[new $mon]") as "mon".
{ iExists _, _. iFrame. done. }
by rewrite insert_id; try assumption.
Qed.
(* Reinsert a node that has been taken out. *)
Lemma reinsert_node γ q s ι n (m : gmap loc (gname * loc)) :
own γ ( (to_agree <$> m) : nodeUR) -
node_mapsto γ s ι n -
([ map] s a (delete s m), ( ι n', a = (ι, n') sentinelInv ι q s n')) -
sentinelInv ι q s n
-
own γ ( (to_agree <$> m) : nodeUR)
( [ map] s a (delete s m), ( ι n, a = (ι, n) sentinelInv ι q s n)).
([ map] s a m, ( ι n', a = (ι, n') sentinelInv ι q s n')).
Proof.
iIntros "ownM mon frag".
iIntros "ownM frag mon new".
iDestruct (big_sepM_insert_delete with "[new $mon]") as "mon".
{ iExists _, _. iFrame. done. }
iDestruct (own_valid_2 with "ownM frag") as %[inc _]%auth_both_valid.
pose proof (map_singleton_included m s (ι, n) inc) as isSome.
rewrite insert_id.
2: { apply (map_singleton_included m s (ι, n) inc). }
iFrame.
Qed.
Lemma node_lookup_subset γ (ι : gname) (q s n : loc) (m m' : gmap loc (gname * loc)) :
m m'
own γ ( (to_agree <$> m) : nodeUR) -
( [ map] s a m', ( ι n, a = (ι, n) sentinelInv ι q s n)) -
node_mapsto γ s ι n -
( sentinelInv ι q s n)
own γ ( (to_agree <$> m) : nodeUR)
( [ map] s a (delete s m'), ( ι n, a = (ι, n) sentinelInv ι q s n)).
Proof.
iIntros (sub) "ownM mon frag".
iDestruct (auth_node_mapsto_Some with "ownM frag") as %S.
iDestruct (big_sepM_later with "mon") as "mon".
iDestruct (big_sepM_delete with "mon") as "[singl mon]"; first done.
iDestruct (big_sepM_delete with "mon") as "[singl mon]".
{ eapply lookup_weaken; done. }
iDestruct "singl" as (a b) "[eq sentInv]".
iDestruct (big_sepM_later with "mon") as "mon".
iFrame.
......@@ -199,6 +296,15 @@ Section Queue_refinement.
iFrame.
Qed.
Lemma node_lookup γ (ι : gname) (q s n : loc) (m : gmap loc (gname * loc)) :
own γ ( (to_agree <$> m) : nodeUR) -
( [ map] s a m, ( ι n, a = (ι, n) sentinelInv ι q s n)) -
node_mapsto γ s ι n -
( sentinelInv ι q s n)
own γ ( (to_agree <$> m) : nodeUR)
( [ map] s a (delete s m), ( ι n, a = (ι, n) sentinelInv ι q s n)).
Proof. iApply node_lookup_subset. done. Qed.
Fixpoint xsLink (τi : D) (xs xs : list val) : iProp Σ :=
match (xs, xs) with
| (nil, nil) => True
......@@ -361,19 +467,18 @@ Section Queue_refinement.
(* Allocate the nodes invariant. *)
iMod (own_alloc ( nodeSentinel nodeSentinel)) as (ι) "[authNodeSentinel fragNodeSentinel]".
{ by apply auth_both_valid. }
(* iMod (own_alloc (● {[ ℓsentinel := (ι, tail) ]} ⋅ ◯ {[ ℓsentinel := (ι, tail) ]})) as (γ) "ownO".
{ apply auth_both_valid. done. } *)
(* iMod (own_alloc (● (node_singleton ℓsentinel ι tail) ⋅ ◯ (node_singleton ℓsentinel ι tail))) as (γ) "ownO".
{ apply auth_both_valid. split; first done. apply singleton_valid. } *)
iMod (own_alloc ( {[ sentinel := to_agree (ι, tail) ]} {[ sentinel := to_agree (ι, tail) ]})) as (γ) "ownO".
{ apply auth_both_valid. split; first done. by apply singleton_valid. }
{ apply auth_both_valid. split; first done. admit. (* apply singleton_valid. *) }
iDestruct "ownO" as "[authO fragO]".
iMod (inv_alloc sentinelN _ (nodesInv γ q) with "[authO fragNodeSentinel qPts']") as "#nodesInv".
{ iNext. iExists {[sentinel := (ι, tail)]}. iSplitL "authO".
(* { iAssumption. } *)
{ admit. }
admit.
(* rewrite big_sepM_singleton. *)
{ (* apply map_fmap_singleton. *) admit. }
rewrite big_sepM_singleton.
iExists _, _. iSplitR; auto.
iExists _, _. admit.
(* iApply (big_sepM_singleton _ ℓsentinel (ι, tail)). } *)
}
(* We now want to allocate the invariant for the queue. To do that we first
establish the node invariant for the empty node we have created. *)
......@@ -419,7 +524,6 @@ Section Queue_refinement.
iMod (own_update with "nodeState") as "[authNodeState nodeState]".
{ by apply (auth_update_core_id_frac _ nodeSentinel). }
iApply (wp_load with "qPts"). iNext. iIntros "qPts".
(* iDestruct (splitIsNodeList with "nodeList") as "[nodeList first]". *)
iMod ("Hclose" with "[qPts lofal Hlink Hsq sentinelPts' authNodeState nodeList nodeinv]") as "_".
{ iNext. iExists _, _, _.
iFrame.
......@@ -454,7 +558,7 @@ Section Queue_refinement.
iInv nodeN as (other q0) "[>Left | Right]" "closeNodeInv".
+ (* xs is the empty list *)
iDestruct "Left" as "(hdPtPts & [otherPts otherPts'] & tok)".
iApply (wp_load with "[$hdPtPts]"). iNext. iIntros "hdPtPts".
(* iApply (wp_load with "[$hdPtPts]"). iNext. iIntros "hdPtPts". *)
simpl.
iInv queueN as ('2 xs2 xs2) "(isMSQ & >-> & >Hsq & >lofal & Hlink & >%)" "closeQueueInv".
rewrite /isMSQueue.
......@@ -467,7 +571,7 @@ Section Queue_refinement.
(* We destruct the sentinel invariant and establish contradictions in
the first and the last disjunct as we can infer that the sentinel we
read earlier is still the sentinel. *)
iDestruct "sentInv" as (v3 q3) "(sntPtsUnused & [[ownO fst]|[snd | >thrd]])".
iDestruct "sentInv" as (v3 q3) "(sentPts & [[ownO fst]|[snd | >thrd]])".
3: {
iDestruct (own_valid_2 with "thrd nodeState") as %[_ [eq%mnat_included _]]%auth_both_frac_valid.
inversion eq.
......@@ -478,12 +582,6 @@ Section Queue_refinement.
iDestruct (mapsto_agree with "otherPts nodePts") as %[=].
}
iDestruct "snd" as ">(nodeState2 & qPts2)".
(* iInv sentinelN as (m) "[>qPts2|(tok' & next)]" "closeSentinelInv".
2: {
iDestruct "next" as (q1 ℓnode a b) ">(hdPtPts2 & nodePts)".
iDestruct (mapsto_agree with "hdPtPts hdPtPts2") as %[= ->].
iDestruct (mapsto_agree with "otherPts nodePts") as %[=].
} *)
(* We can conclude that the queue still points to the same sentinel that
we read previously. *)
iDestruct (mapsto_agree with "qPts qPts2") as %[= ->].
......@@ -503,15 +601,20 @@ Section Queue_refinement.
(* We now step over the specification code. *)
iMod (steps_CG_dequeue_nil with "[$Hspec $Hj $Hsq $lofal]") as "(Hj & Hsq & lofal)".
{ solve_ndisj. }
iApply (wp_load with "[$hdPtPts]"). iNext. iIntros "hdPtPts".
(* We now close all the invariants that we opened. *)
iDestruct (reinsert_node with "authM fragO bigSep [sentPts nodeState2 qPts2]") as "(authM & bigSep)".
{ iExists _, _. iFrame. iRight. iLeft. iFrame. }
iMod ("closeNodesInv" with "[authM bigSep]") as "_".
{ iNext. iExists _. iFrame. }
iModIntro.
iMod ("closeQueueInv" with "[qPts lofal Hsq sentinelPts nodeList nodeState']") as "_".
{ iNext. iExists _, [], _.
iFrame.
iSplit; auto.
iExists _, _, _, _, _, _. iFrame. iFrame "nodeinv' fragO'".
}
iModIntro.
iMod ("closeNodeInv" with "[hdPtPts otherPts' tok]").
{ iNext. iExists _, _. iLeft. iFrame. }
iModIntro.
......@@ -546,12 +649,11 @@ Section Queue_refinement.
rewrite /isMSQueue.
iDestruct "isMSQ" as (sentinel2 v2 hdPt2 q2 ι' κ')
"(>qPts & >sentinelPts' & >#fragO' & >sentinelState & nodeList & #nodeinv')".
(* iClear "senInv". *)
(* We now open the nodes invariant. *)
iInv sentinelN as (m) "[>authM bigSep]" "closeNodesInv".
iDestruct (node_lookup with "authM bigSep fragO'") as "(sentInv & authM & bigSep)".
iDestruct "sentInv" as (v3 q3) "(sentPts & [[>ownO _]|[>snd| >ownO]])";
try iDestruct (own_valid_2 with "sentinelState ownO") as %[=]%auth_auth_frac_op_invL.
try iDestruct (state_agree with "sentinelState ownO") as %[=].
iDestruct "snd" as "(ownO & qPts2)".
iCombine "sentinelState ownO" as "sentinelState".
iDestruct (mapsto_combine with "qPts qPts2") as "[qPts %]".
......@@ -588,8 +690,22 @@ Section Queue_refinement.
}
destruct xs2 as [|x2' xs2']; simpl.
{ inversion H7. }
iDestruct "nodeList" as (tail next q1 ι2) "(frag & nodeState' & hdPts'' & tailPts & nodeList)".
iDestruct (mapsto_agree with "hdPts hdPts''") as %[= <-].
iDestruct "nodeList" as (tail next q1 ι2) "(#frag & nodeState' & hdPts'' & tailPts & nodeList)".
iDestruct (mapsto_agree with "hdPts hdPts''") as %[= ->].
iDestruct (auth_node_mapsto_Some with "authM fragO'") as %sentSome.
iAssert (delete sentinel m !! tail = Some (ι2, next)%I) as %Eq.
{ iDestruct (auth_node_mapsto_Some with "authM frag") as %Eq.
destruct (decide (sentinel = tail)) as [->|Neq].
- (* We derive a contradiction. *)
iDestruct (node_mapsto_agree with "fragO' frag") as %[-> B].
iDestruct (state_agree with "nodeState' sentinelState") as %[=].
- 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 [= <- <-] v' q'') "(hdPtPts & [[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 "Hlink" as "[Hτi Hlink]".
(* We step through the specificaion code. *)
......@@ -598,11 +714,19 @@ Section Queue_refinement.
(* We split qPts again such that we can put one half in the sentinel
invariant and one half directly in the queue invariant. *)
iDestruct "qPts" as "[qPts qPts']".
iMod (update_sentinel_dead with "sentinelState") as "sentinelState".
(* iDestruct (big_sepM_insert_delete with "[$bigSep]") as "bigSep". *)
iDestruct (reinsert_node_subset with "bigSep [qPts' nodeState2 hdPtPts]") as "bigSep".
{ eassumption. }
{ iExists _, _. iFrame. iRight. iLeft. iFrame. }
iDestruct (reinsert_node_subset with "bigSep [sentPts sentinelState hdPts'' tailPts]") as "bigSep".
{ apply sentSome. }
{ iExists _, _. iFrame. iLeft. iFrame. iExists _, _, _, _. iFrame. }
iMod ("closeNodesInv" with "[authM bigSep]") as "_".
{ iNext. iExists _. iFrame. }
iModIntro.
(* We are now ready to reestablish the invariant. *)
iMod ("Hclose" with "[qPts lofal Hlink Hsq nodeList hdPts hdPts'' otherPts' tailPts hdPts3 otherPts newSenTok]") as "_".
iMod ("Hclose" with "[qPts lofal Hlink Hsq nodeList hdPts otherPts' hdPts3 otherPts nodeState1]") as "_".
{ iNext.
iDestruct (mapsto_agree with "hdPts hdPts3") as %[= <-].
iDestruct (mapsto_agree with "otherPts' otherPts") as %[= <- <-].
......@@ -610,7 +734,7 @@ Section Queue_refinement.
iExists _, xs2', xs2'.
iFrame.
iSplit; auto.
iExists _ ,_, _, _, _. iFrame. iFrame "tailInv". iAssumption.
iExists _ ,_, _, _, _, _. iFrame. iFrame "tailInv". iAssumption.
}
(* Step over the remainder of the code. *)
iModIntro. simpl.
......
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