Commit f35fcdad authored by William Mansky's avatar William Mansky

First-pass specs for kvgroup.

parent 2818a1b2
......@@ -26,47 +26,49 @@ Qed.
Section kvnode.
Context `{!noprolG Σ,
kvprot: !gpsSimplG Σ (nat * list Z) ghistProtocol,
(* should the version numbers for the component kvnodes be included here? *)
kvprot: !gpsSimplG Σ (nat * list (list Z)) Prtcl,
kvgprot: !gpsSimplG Σ (nat * list (list Z)) Prtcl,
gpGv: !gpsG Σ (versionProtocol Prtcl),
gpGd: !gpsG Σ histProtocol,
gpGp: !gpsG Σ ptrProtocol}.
Local Notation vProp := (vProp Σ).
Section definitions.
sGPS_iSP_Reader
Definition gdataP (n: loc) γv : interpSC Σ (nat * list Z) ghistProtocol :=
(λ _ _ _ s '(_, vals), log_latest s ver vals t tsm,
(λ _ _ _ s v, ver, log_latest s ver v.2 t tsm,
GPS_SWReader (Prtcl:=(versionProtocol Prtcl)) (n >> version) t
((ver - 1)%nat, tsm) #(ver - 1)%nat γv)%I.
Global Instance dataP_persistent n γv b tv s v :
Persistent (dataP n γv b γv tv s v) := _.
Definition dataObs (n: loc) L γs γv:=
Global Instance dataP_persistent n γv b l tv s v :
Persistent (gdataP n γv b l tv s v) := _.
Definition dataObs (n: loc) GL γs γv:=
([ list] i↦γi γs, ti vi,
(* Do we need the whole kvnode_prots_R here? *)
sGPS_iSP_Reader (kvgroupN n) (gdataP n γv) ti (map_nth i L O) vi γi)%I.
(* Do we need the whole kvnode_prots_R here? Or maybe it should just be
pointer observations? *)
sGPS_iSP_Reader (kvgroupN n) (gdataP n γv) ti (map_nth i GL []) vi γi)%I.
Definition gversionP (n: loc) γm γs : interpC Σ (versionProtocol Prtcl) :=
(λ _ _ γv _ s v, v = #(Z.of_nat s.1)
if even s.1 then
( L vs, map_size L Nd log_latest L s.1 vs
( GL vs, map_size GL Nd log_latest GL s.1 vs
(* observation of the data locations *)
dataObs n L γs γv
dataObs n GL γs γv
(* observation of the library-level value *)
(sGPS_SWReader (Prtcl:=Prtcl) s.2.1 s.2.2 (s.1, vs) γm))
else True)%I.
Definition ptrP (n: loc) : interpC Σ ptrProtocol :=
(λ b _ _ _ s v, v = #s
if b then kvnode_prots_W ? (kvgroupN n) s ? ? ? ? state (ver, vals)
else kvnode_prots_R ? (kvgroupN n) s ? ? ? ? state (ver, vals)).
Definition ptrP (n: loc) γv : interpC Σ ptrProtocol :=
(λ _ _ _ _ s v, v = #(LitLoc s)
L ti vi γi, sGPS_iSP_Reader (kvgroupN n) (gdataP s γv) ti L vi γi)%I.
End definitions.
(*Instance versionP_persistent n γm γs b l γv tv s v :
Persistent (versionP n γm γs b l γv tv s v).
Proof. apply bi.sep_persistent; [apply _|]. case (even s.1); apply _. Qed.*)
Instance gversionP_persistent n γm γs b l γv tv s v :
Persistent (gversionP n γm γs b l γv tv s v).
Proof. apply bi.sep_persistent; [apply _|]. case (even s.1); apply _. Qed.
(*Section helpers.
Lemma node_state_ord L1 L2 v1 v2 n γs γv E
......@@ -195,33 +197,32 @@ Proof. apply bi.sep_persistent; [apply _|]. case (even s.1); apply _. Qed.*)
Qed.
End helpers.*)
Context (IP : interpSC Σ (nat * list Z) Prtcl).
Context (IP : interpSC Σ (nat * list (list Z)) Prtcl).
Context (N : namespace).
Context (n : loc).
Context (γm γv: gname) (γs : list gname).
(** kvnode_prots_R/W are the library-level reader/writer assertion. *)
Definition kvnode_prots_W t s v :=
( L, length γs = Nd map_size L Nd log_latest L v.1 v.2
(** kvgroup_prots_R/W are the library-level reader/writer assertion. *)
Definition kvgroup_prots_W t s v :=
( GL, length γs = Nd map_size GL Nd log_latest GL v.1 v.2
(* Single-Writer of version location *)
( tv, GPS_iSP_Writer (kvnodeN n) (versionP n γm γs)
(versionP n γm γs false)
( tv, GPS_iSP_Writer (kvgroupN n) (gversionP n γm γs)
(gversionP n γm γs false)
(n >> version) tv (v.1, (t,s)) #v.1 γv)
(* Single-Writers of data locations *)
([ list] i↦γi γs, ti vi,
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)
sGPS_iSP_Writer (kvgroupN n) (gdataP n γv) ti (map_nth i GL []) vi γi)
(* Single-Writer of the library-level protocol *)
sGPS_iSP_Writer N IP t s 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
Definition kvgroup_prots_R t s v :=
( GL, length γs = Nd map_size GL Nd log_latest GL v.1 v.2
(* Reader of version location *)
( tv, GPS_iSP_Reader (kvnodeN n) (versionP n γm γs)
(versionP n γm γs false)
( tv, GPS_iSP_Reader (kvgroupN n) (gversionP n γm γs)
(gversionP n γm γs false)
(n >> version) tv (v.1, (t,s)) #v.1 γv)
(* Readers of data locations *)
dataObs n L γs γv
dataObs n GL γs γv
(* Reader of the library-level protocol *)
sGPS_iSP_Reader N IP t s v γm)%I.
......@@ -231,13 +232,13 @@ Notation F_past := (IP false γm). (* read interp *)
Lemma write_spec ain t s v vals t' s' vals' (R : time vProp) tid E
(Hlen: length vals' = Nd) (Exts: s s') (Ext: (t < t')%positive)
(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 t s (v, vals)
{{{ ([ list] ix List.concat vals', (ain >> Z.of_nat i) #(LitInt x))
kvgroup_prots_W 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') }}}
write [ #n; #ain] in tid @ E
{{{ RET #; ([ list] ix vals', (ain >> Z.of_nat i) #(LitInt x))
kvnode_prots_W t' s' ((v + 2)%nat, vals') R t' }}}.
write_all [ #n; #ain] in tid @ E
{{{ RET #; ([ list] ix List.concat vals', (ain >> Z.of_nat i) #(LitInt x))
kvgroup_prots_W t' s' ((v + 2)%nat, vals') R t' }}}.
Proof.
iIntros (Φ) "(Hdata & Hwrite & Hstep) Hpost".
wp_lam. rewrite {1}/subst. simpl_subst. (* TODO: why do we need this? *)
......
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