Commit a497f6cc authored by William Mansky's avatar William Mansky

Added location to "value" of kvnode protocol.

parent 81478f61
......@@ -33,8 +33,7 @@ Definition historyR := snapR (gmapUR nat (agreeR (prodC (discreteC loc) (gmapC n
Section kvnode.
Context `{!noprolG Σ,
kvprot: !gpsSimplG Σ (nat * list Z) ghistProtocol,
(* should the version numbers for the component kvnodes be included here? *)
kvprot: !gpsSimplG Σ (loc * (nat * list Z)) ghistProtocol,
kvgprot: !gpsSimplG Σ (nat * list (list Z)) Prtcl,
gpGv: !gpsG Σ (versionProtocol ghistProtocol),
gpGd: !gpsG Σ histProtocol,
......@@ -50,8 +49,9 @@ Section definitions.
Definition hist_master q γh PL : vProp :=
own γh (#{q} (to_agree <$> PL) : historyR)%I.
Definition gdataP (n: loc) γv γh : interpSC Σ (nat * list Z) ghistProtocol :=
(λ _ _ _ s v, ver PL pver p, log_latest s ver v.2 /\ log_latest PL pver (p, s) hist_snapshot γh PL t tsm,
Definition gdataP (n: loc) γv γh : interpSC Σ (loc * (nat * list Z)) ghistProtocol :=
(λ _ _ _ s v, ver PL pver, log_latest s ver v.2.2 /\ log_latest PL pver (v.1, s) /\ length v.2.2 = Nd
hist_snapshot γh PL t tsm,
GPS_SWReader (Prtcl:=(versionProtocol Prtcl)) (n >> version) t
((ver - 1)%nat, tsm) #(ver - 1)%nat γv)%I.
......@@ -420,9 +420,9 @@ Proof.
rewrite bi.sep_assoc; iSplit; [|done].
rewrite <- bi.persistent_sep_dup; try typeclasses eauto.
iNext; unfold gdataP.
iDestruct "data" as (????) "(% & _ & data)".
iDestruct "data" as (???) "(% & _ & data)".
iDestruct "snap" as (?? pver PL) "[[% %] snap]".
iExists (v + 2)%nat, _, _, _. iSplit; last first.
iExists (v + 2)%nat, _, _. iSplit; last first.
- iFrame "#". iExists t1. rewrite (_: (v + 2 - 1)%nat = (v + 1)%nat); [|lia].
rewrite (_: (Z.of_nat v + 1) = (v + 1)%nat); [|lia].
iExists _. iDestruct "Rv" as "[$ ?]".
......@@ -558,7 +558,7 @@ Proof.
(* loop invariant *)
set φ : Z vProp :=
(λ i : Z, i Nd vals, i = Z.of_nat (length vals)
([ list] jl vals, [ list] kx l, (out >> (j * Nd + k)) #(LitInt x))
([ list] jl vals, length l = 8%nat [ list] kx l, (out >> (j * Nd + k)) #(LitInt x))
([ list] j seq (Z.to_nat i) (Nd - Z.to_nat i), ([ list] k seq 0 Nd, (out >> (Z.of_nat j * Nd + Z.of_nat k)) -))
v', (v1 v' - 1)%nat
(▷∃ tv ts' ss', ts1 ts' ss1 ss'⌝
......@@ -607,8 +607,9 @@ Proof.
iDestruct "KVi" as (ni ? (?, ?) pver0 L pver ? PL') "((% & % & % & % & %) & snap' & KVi)"; subst p.
(* reading *)
wp_op. wp_op.
iApply wp_fupd.
(* Two cases: location is the same, or KVi is more up-to-date than Hdi. *)
iApply (read_spec (gdataP n γv γh) (kvgroupN n) _ _ _ _ _ _ _ _ _ (fun t s v => gdataP n γv γh false γm' t s v)%I (fun t s v => gdataP n γv γh false γm' t s v)%I
iApply (read_spec (gdataP n γv γh) (kvgroupN n) _ _ _ _ _ _ _ _ _ (fun t s v => gdataP n γv γh false γm' t s (ni, v))%I (fun t s v => gdataP n γv γh false γm' t s (ni, v))%I
with "[outi $KVi]"); try done. (* We have two kvprot snapshots here: one from the pointer, and one from the previous read.
The previous read may be from a different location. *)
{ iSplitR "".
......@@ -619,12 +620,14 @@ Proof.
iIntros "!>" (ti' si' vi' vals') "(Exti & out & #kvi & HdP)".
(* re-establish loop invariant *)
iApply "Post".
iSplit; first by iPureIntro; lia.
iExists (vals0 ++ [vals']). iSplit.
iSplitL ""; first by iPureIntro; lia.
iExists (vals0 ++ [vals']). iSplitL "".
{ iPureIntro. rewrite app_length EqL /=. lia. }
iDestruct "HdP" as (veri PL1 pver1 (? & ? & ?)) "#[snap1 kVeri]".
rewrite big_sepL_app. iSplitL "Hout out".
{ iClear "#". iFrame "Hout". rewrite /= Nat.add_0_r -EqL.
iSplit; last done.
iModIntro; iSplit; last done.
iSplit; first done.
iApply (big_sepL_mono with "out"); intros; simpl.
by rewrite shift_lblock_assoc Z.mul_comm. }
iSplitL "Hrest".
......@@ -637,16 +640,14 @@ Proof.
- rewrite (_ : (ri = S ri - 1)%nat); last lia.
rewrite -Hi Z2Nat.inj_add; [|lia..]. by rewrite Nat.sub_add_distr. }
iDestruct "Exti" as %[? Extvi].
iDestruct "HdP" as (veri) "#HdP".
iExists (Nat.max v' veri). iSplit.
iExists (Nat.max v' veri). iSplitL "".
{ iPureIntro. rewrite -Nat.sub_max_distr_r.
etrans; [apply Lev'|apply Nat.le_max_l]. } iSplitL "".
{ iNext. iDestruct "HdP" as (????) "[snap' #kVeri]".
destruct LL1 as [vs1 Ll1].
{ destruct LL1 as [vs1 Ll1].
iDestruct "kVeri" as (tvi [tsi ssi]) "kVeri".
(* iAssert (|={E}=> (v' - 1)%nat (veri - 1)%nat ts' tsi ss' ssi
(*iAssert (|={E}=> (v' - 1)%nat (veri - 1)%nat ts' tsi ss' ssi
(veri - 1)%nat (v' - 1)%nat tsi ts' ssi ss'⌝)%I
as "Case".
as ">Case".
{ iMod (GPS_iSP_Readers_agree _ (versionP n γm' γs') with "kv' [$kVeri]")
as "Le"; [done|by iDestruct "kv'" as "[? $]"|].
iClear "#". iIntros "!>".
......@@ -658,7 +659,7 @@ Proof.
iPureIntro. split; by etrans.
- rewrite Nat.max_l; [iFrame "kv'"|done].
iPureIntro. split; by etrans.*) admit. }
rewrite big_sepL_app. iSplitL "Hvals".
iModIntro. rewrite big_sepL_app. iSplitL "Hvals".
{ iApply (big_sepL_mono with "Hvals"). simpl.
iIntros (j dj Eqj). iDestruct 1 as (Lj vj) "[Eqj HRj]".
iExists Lj, vj. iFrame "HRj". iDestruct "Eqj" as %[[Le1 Le2] [Ll SubL]].
......@@ -668,7 +669,6 @@ Proof.
iExists si', veri. iSplit.
{ (*iPureIntro. split; split; auto. apply Nat.le_max_r.
rewrite Nat.add_0_r. move : Extvi. by rewrite EqL Nat2Z.id.*) admit. }
iDestruct "HdP" as (PL1 pver1 ?) "([% %] & snap1 & ?)".
iExists PL1, pver0, L, pver1, t', ti', ni, s'; iExists (vi', vals'), (γi, (γm', γv', γs', γh)). rewrite Nat.add_0_r. iSplit; last by rewrite EqL; auto.
iPureIntro. move : Hγi. by rewrite EqL Nat2Z.id.
(* done with loop invariant *) }
......@@ -704,8 +704,8 @@ Proof.
rewrite Even. iDestruct "VP" as (L3 vs3) "(MS3 & DO3 & #Rm3)".
iDestruct "MS3" as %[MS3 LL3].
have Eqv1: (v1 = v' - 1)%nat by apply (anti_symm ()%nat).
iDestruct (log_latest_comprehend _ _ γs' _ _ vals' with "[Hvals]")
as (L') "[ALL DOL']"; [eauto|by rewrite Lenγ|..].
iDestruct (log_latest_comprehend _ _ γs _ _ vals' with "[Hvals]")
as (GL') "[ALL DOL']"; [eauto|by rewrite Lenγ|..].
{ iApply (big_sepL_mono with "Hvals").
iIntros (i zi Eqi). simpl.
iDestruct 1 as (Lj vj [[Gej Lej] [LLj Subj]]) "Hj".
......@@ -715,7 +715,7 @@ Proof.
have ?: vj = v'. { apply (anti_symm ()%nat); lia. } subst vj.
exfalso. move : Even. rewrite Nat.even_sub; [|lia]. by rewrite Evenj. }
iDestruct "ALL" as %[MS' [LL' ALL']].
iMod (node_state_ord L' L3 v1 v1 _ γs with "[#] [#]") as %ExtL3;
iMod (gdataObs_ord GL' L3 v1 v1 _ γs with "[#] [#]") as %ExtL3;
[done|done|..].
{ iSplit. iPureIntro. move : MS'. move : Len => <- ?. by eauto.
iFrame "DOL'". }
......
......@@ -26,7 +26,8 @@ Qed.
Section kvnode.
Context `{!noprolG Σ,
kvprot: !gpsSimplG Σ (nat * list Z) Prtcl,
(* we include the current location of the data structure in the "value" of the library-level protocol *)
kvprot: !gpsSimplG Σ (loc * (nat * list Z)) Prtcl,
gpGv: !gpsG Σ (versionProtocol Prtcl),
gpGd: !gpsG Σ histProtocol}.
Local Notation vProp := (vProp Σ).
......@@ -54,7 +55,7 @@ Section definitions.
(* observation of the data locations *)
dataObs n L γs γv
(* observation of the library-level value *)
(sGPS_SWReader (Prtcl:=Prtcl) s.2.1 s.2.2 (s.1, vs) γm))
(sGPS_SWReader (Prtcl:=Prtcl) s.2.1 s.2.2 (n, (s.1, vs)) γm))
else True)%I.
End definitions.
......@@ -189,7 +190,7 @@ Section helpers.
Qed.
End helpers.
Context (IP : interpSC Σ (nat * list Z) Prtcl).
Context (IP : interpSC Σ (loc * (nat * list Z)) Prtcl).
Context (N : namespace).
Context (γm γv: gname) (γs : list gname).
......@@ -209,7 +210,7 @@ Definition kvnode_prots_W t s v :=
GPS_iSP_Writer (kvnodeN n) (dataP n γv) (dataP n γv false)
(n >> data >> (Z.of_nat i)) ti (map_nth i L O) vi γi)
(* Single-Writer of the library-level protocol *)
sGPS_iSP_Writer N IP t s v γm)%I.
sGPS_iSP_Writer N IP t s (n, v) γm)%I.
Definition kvnode_prots_R t s v :=
( L, length γs = Nd map_size L Nd log_latest L v.1 v.2
......@@ -220,7 +221,7 @@ Definition kvnode_prots_R t s v :=
(* Readers of data locations *)
dataObs n L γs γv
(* Reader of the library-level protocol *)
sGPS_iSP_Reader N IP t s v γm)%I.
sGPS_iSP_Reader N IP t s (n, v) γm)%I.
Lemma kvnode_prots_WR : forall t s v,
kvnode_prots_W t s v - kvnode_prots_R t s v.
......@@ -255,16 +256,18 @@ Proof.
by iApply (sGPS_iSP_Readers_agree with "R1 R2").
Qed.
Lemma kvnode_Readers_agree' : forall n1 n2 t1 t2 s1 s2 v1 v2 E, N E -> s1 s2 ->
(*Lemma kvnode_Readers_agree' : forall n1 n2 t1 t2 s1 s2 v1 v2 E, N E -> s1 s2 ->
kvnode_prots_R n1 t1 s1 v1 - kvnode_prots_R n2 t2 s2 v2 ={E}=
kvnode_prots_R n1 t2 s2 v2.
Proof.
intros; unfold kvnode_prots_R.
iIntros "R1 R2".
iDestruct "R1" as (??) "(_ & _ & R1)".
iDestruct "R2" as (??) "(_ & _ & R2)".
iDestruct "R1" as (L ?) "(? & ? & R1)".
iDestruct "R2" as (??) "(? & ? & R2)".
iModIntro.
iExists L; iSplit; auto.
by iApply (sGPS_iSP_Readers_agree with "R1 R2").
Qed.
Qed.*)
(* kvnode_prots_W/R should be considered the "real" protocol assertions for kvnode,
and users should not use sGPS_iSP_Reader (since it doesn't include protocol assertions
......@@ -280,8 +283,8 @@ Lemma write_spec ain t s v vals t' s' vals' (R : time → vProp) tid E
(DISJ: histN ## N) (SUB1: histN E) (SUB2: N E) (SUB3: kvnodeN n E) :
{{{ ([ list] ix vals', (ain >> Z.of_nat i) #(LitInt x))
kvnode_prots_W n t s (v, vals)
( F t s (v, vals) ={E N}= F t' s' ((v + 2)%nat, vals')
F_past t' s' ((v + 2)%nat, vals') R t') }}}
( F t s (n, (v, vals)) ={E N}= F t' s' (n, ((v + 2)%nat, vals'))
F_past t' s' (n, ((v + 2)%nat, vals')) R t') }}}
write [ #n; #ain] in tid @ E
{{{ RET #; ([ list] ix vals', (ain >> Z.of_nat i) #(LitInt x))
kvnode_prots_W n t' s' ((v + 2)%nat, vals') R t' }}}.
......@@ -388,7 +391,7 @@ Proof.
have ? : v8 = 8 by lia. subst v8. clear φ Le8 Ge8.
wp_seq. wp_op. wp_op.
(* commit point: write new even version *)
iMod (sGPS_iSP_Write N IP t s (v, vals) _ t' s' ((v + 2)%nat, vals') R
iMod (sGPS_iSP_Write N IP t s (n, (v, vals)) _ t' s' (n, ((v + 2)%nat, vals')) R
with "Hstep Wm") as "[Wm R]"; [done..|].
iDestruct (sGPS_iSP_SWWriter_Reader with "Wm") as "#Rm".
rewrite take_ge; last by (rewrite Hlen Nat2Z.inj_le Z2Nat.id; lia).
......@@ -433,8 +436,8 @@ Lemma read_spec (out: loc) t s v vals
{{{ ([ list] i seq O Nd, (out >> Z.of_nat i) -)
kvnode_prots_R n t s (v, vals)
<obj> ( t' s' vvals', (t t')%positive s s'⌝ -
( F_past t' s' vvals' ={E N}= F_past t' s' vvals' R t' s' vvals')
( F t' s' vvals' ={E N}= F t' s' vvals' R t' s' vvals'))
( F_past t' s' (n, vvals') ={E N}= F_past t' s' (n, vvals') R t' s' vvals')
( F t' s' (n, vvals') ={E N}= F t' s' (n, vvals') R t' s' vvals'))
( t' s' vvals', (t t')%positive s s'⌝ -
R t' s' vvals' ={E N}= Q t' s' vvals') }}}
read [ #n ; #out] in tid @ E
......@@ -617,7 +620,7 @@ Proof.
have Ext': (t ts2)%positive s ss2.
{ split; by do 2 etrans. }
(* commit point, accessing the library-level protocol *)
iMod (sGPS_iSP_Read N IP ts2 ss2 (v1, vals') γm Q R with "[VS1] [VS2] [$Rm3]")
iMod (sGPS_iSP_Read N IP ts2 ss2 (n, (v1, vals')) γm (fun t s '(_, v) => Q t s v) (fun t s '(_, v) => R t s v) with "[VS1] [VS2] [$Rm3]")
as "Q"; [done|..|by iDestruct "Rm" as "[? $]"|].
{ iIntros "!>". rewrite monPred_objectively_elim.
by iApply ("VS1" $! ts2 ss2 (v1, vals')). }
......
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