Commit e864e9c5 authored by William Mansky's avatar William Mansky

Some progress on kvgroup.

parent baeebf86
......@@ -16,6 +16,7 @@ Definition kvgroupN (n: loc) := nroot .@ "kvnodeN" .@ n.
Canonical Structure ghistProtocol : protocolT :=
Build_protocolT (gmap nat (list Z)) _ _ _ map_subseteq _.
(*
(* Maybe this will need to be "set once" or even static. *)
Program Definition ptrProtocol : protocolT :=
Build_protocolT loc _ _ _ (fun _ _ => True) _.
......@@ -23,15 +24,17 @@ Next Obligation.
Proof.
constructor; repeat intro; auto.
Qed.
*)
Section kvnode.
Context `{!noprolG Σ,
kvprot: !gpsSimplG Σ (nat * list Z) ghistProtocol,
(* should the version numbers for the component kvnodes be included here? *)
kvgprot: !gpsSimplG Σ (nat * list (list Z)) Prtcl,
gpGv: !gpsG Σ (versionProtocol Prtcl),
gpGv: !gpsG Σ (versionProtocol ghistProtocol),
gpGd: !gpsG Σ histProtocol,
gpGp: !gpsG Σ ptrProtocol}.
gpGv': !gpsG Σ (versionProtocol Prtcl),
gpGp: !gpsG Σ ghistProtocol}.
Local Notation vProp := (vProp Σ).
Section definitions.
......@@ -60,9 +63,10 @@ Section definitions.
(sGPS_SWReader (Prtcl:=Prtcl) s.2.1 s.2.2 (s.1, vs) γm))
else True)%I.
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.
Definition ptrP (n: loc) γv : interpC Σ ghistProtocol :=
(λ b _ _ _ s v, p ti vi γm' γv' γs', v = #(LitLoc p)
if b then kvnode_prots_W (gdataP p γv) (kvgroupN n) p γm' γv' γs' ti s vi
else kvnode_prots_R (gdataP p γv) (kvgroupN n) p γm' γv' γs' ti s vi)%I.
End definitions.
......@@ -210,12 +214,15 @@ Definition kvgroup_prots_W t s v :=
(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,
sGPS_iSP_Writer (kvgroupN n) (gdataP n γv) ti (map_nth i GL []) vi γi)*)
([ list] i↦γi γs, ti vi,
sGPS_iSP_Writer (kvgroupN n) (gdataP n γv) ti (map_nth i GL []) vi γi)
GPS_iSP_Writer (kvgroupN n) (ptrP n γv) (ptrP n γv false) (n >> data >> i)
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 kvgroup_prots_R t s v :=
(*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 (kvgroupN n) (gversionP n γm γs)
......@@ -224,12 +231,12 @@ Definition kvgroup_prots_R t s v :=
(* Readers of data locations *)
dataObs n GL γ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 v γm)%I.*)
Notation F := (IP true γm). (* full interp *)
Notation F_past := (IP false γm). (* read interp *)
Lemma write_spec ain t s v vals t' s' vals' (R : time vProp) tid E
Lemma write_all_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 List.concat vals', (ain >> Z.of_nat i) #(LitInt x))
......@@ -241,12 +248,15 @@ Lemma write_spec ain t s v vals t' s' vals' (R : time → vProp) tid E
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? *)
iDestruct "Hwrite" as (L) "(MS & Wv & Wds & Wm)".
wp_lam. (* rewrite {1}/subst. simpl_subst. This doesn't work. --WM *)
unfold subst. simpl. fold (subst "in" #ain write). fold (subst "n" #n (subst "in" #ain write)).
rewrite (is_closed_nil_subst _ "in"); [|apply is_closed_of_val].
rewrite is_closed_nil_subst; [|apply is_closed_of_val].
iDestruct "Hwrite" as (GL) "(MS & Wv & Wds & Wm)".
iDestruct "Wv" as (tv) "Wv".
(* read version, this is a single-writer read *)
wp_op. wp_bind (!ᵃᶜ_)%E.
iApply (GPS_iSP_SWRead (kvnodeN n) (versionP n γm γs)%I _ True%I
iApply (GPS_iSP_SWRead (kvgroupN n) (gversionP n γm γs)%I _ True%I
with "[$Wv]"); [solve_ndisj|done|done|by right|..].
{ by iIntros "!> !> $". }
iIntros "!> [Wv _]". wp_let.
......@@ -254,7 +264,7 @@ Proof.
have Even := log_latest_even _ _ _ LL.
(* increment version to prepare writing *)
do 2 wp_op. wp_bind (_ <-ʳᵉˡ _)%E.
iApply (GPS_iSP_SWWrite (kvnodeN n) (versionP n γm γs)%I _ True%I _
iApply (GPS_iSP_SWWrite (kvgroupN n) (gversionP n γm γs)%I _ True%I _
_ _ _ ((v + 1)%nat, (t,s)) _ #(v + 1) with "[$Wv]");
[solve_ndisj|done|done|by right
|repeat split; [by apply Nat.le_add_r|done..]|..].
......@@ -264,12 +274,12 @@ Proof.
by rewrite Nat.even_add Even /=.
- by iIntros "!> !> $". }
iIntros "!>" (t1) "[_ [Wv _]]". wp_seq.
iDestruct (GPS_iSP_SWWriter_Reader _ (versionP n γm γs) with "Wv") as "#Rv".
have SUBL' : L <[(v+2)%nat := vals']>L.
iDestruct (GPS_iSP_SWWriter_Reader _ (gversionP n γm γs) with "Wv") as "#Rv".
have SUBL' : GL <[(v+2)%nat := vals']>GL.
{ apply insert_subseteq.
destruct LL as [_ Hlast].
destruct (Hlast (v + 2)%nat) as [Hnone _].
destruct (L !! (v + 2)%nat) eqn: H2; last done.
destruct (GL !! (v + 2)%nat) eqn: H2; last done.
destruct Hnone; [eauto | lia]. }
have LL' := log_latest_insert _ _ _ vals' LL.
(* for loop *)
......@@ -278,21 +288,34 @@ Proof.
set φ : Z vProp :=
(λ i : Z, 0 i Nd
([ list] ix take (Z.to_nat i) vals', ti vi γi, ⌜γs !! i = Some γi
GPS_iSP_Writer (kvnodeN n) (dataP n γv) (dataP n γv false)
(n >> data >> i) ti
(<[(v + 2)%nat := x]>(map_nth i L O)) vi γi)
GPS_iSP_Writer (kvgroupN n) (ptrP n γv) (ptrP n γv false)
(n >> data >> i) ti (<[(v + 2)%nat := x]>(map_nth i GL [])) vi γi)
([ list] i seq (Z.to_nat i) (8 - Z.to_nat i),
( ti vi γi, ⌜γs !! i = Some γi
GPS_iSP_Writer (kvnodeN n) (dataP n γv) (dataP n γv false)
(n >> data >> (Z.of_nat i)) ti
(map_nth i L 0) vi γi))
([ list] ix vals', (ain >> Z.of_nat i) #(LitInt x)))%I.
GPS_iSP_Writer (kvgroupN n) (ptrP n γv) (ptrP n γv false)
(n >> data >> Z.of_nat i) ti (map_nth i GL []) vi γi))
([ list] ix List.concat vals', (ain >> Z.of_nat i) #(LitInt x)))%I.
iApply (wp_for_simple _ _ 0 "i" Nd with "[] [Wds Hdata]"); [done|..].
{ (* loop invariant maintained *)
instantiate (1 := φ).
iIntros "!>" (i Φ') "!> (LtNd & LeNd & Hwrote & Hrest & in) Post".
iDestruct "LtNd" as %LtNd. iDestruct "LeNd" as %LeNd.
wp_let. wp_op. wp_op. wp_op.
wp_let. wp_op. wp_op.
(* look up ith kvnode *)
wp_bind (!ᵃᶜ_)%E.
destruct (8 - Z.to_nat i)%nat as [|ri] eqn: Hi.
{ exfalso. apply Z2Nat.inj_lt in LtNd; [rewrite Nat2Z.id in LtNd|..]; lia. }
rewrite (big_sepL_cons _ (Z.to_nat i) (seq _ ri)).
iDestruct "Hrest" as "[Hi Hrest]".
iDestruct "Hi" as (ti vli γi Eqγi) "Wi". rewrite Z2Nat.id; [|lia].
iApply (GPS_iSP_SWRead (kvgroupN n) (ptrP n γv)%I _ True%I with "[$Wi]");
[solve_ndisj|done|done|by right
|..].
{ by iIntros "!> !> $". }
iIntros "!> [Wi _]". wp_let.
Check write_spec.
(* read from input *)
wp_bind (!#_)%E.
destruct (lookup_lt_is_Some_2 vals' (Z.to_nat i)) as [vi Eqi].
......@@ -301,11 +324,6 @@ Proof.
rewrite Z2Nat.id; [|lia].
wp_read. iDestruct ("inC" with "ini") as "in".
(* write data *)
destruct (8 - Z.to_nat i)%nat as [|ri] eqn: Hi.
{ exfalso. apply Z2Nat.inj_lt in LtNd; [rewrite Nat2Z.id in LtNd|..]; lia. }
rewrite (big_sepL_cons _ (Z.to_nat i) (seq _ ri)).
iDestruct "Hrest" as "[Hi Hrest]".
iDestruct "Hi" as (ti vli γi Eqγi) "Wi". rewrite Z2Nat.id; [|lia].
iApply (GPS_iSP_SWWrite (kvnodeN n) (dataP n γv)%I _ True%I _ _ _ _
(<[(v + 2)%nat := vi]>(map_nth (Z.to_nat i) L O)) _ #vi
with "[$Wi]"); [solve_ndisj|done|done|by right|..].
......
......@@ -15,13 +15,16 @@ Definition write_all : val :=
"n" + #version <-ʳᵉˡ "v" + #1 ;;
(for: ("i" := #0; "i" < #Nd; "i" + #1)
let: "ni" := !ᵃᶜ("n" + #data + "i") in
(* Right now, ni never changes, so there's no need to do an acquire read.
Could we change that? *)
write ["ni"; "in" + (#Nd * "i")]);;
"n" + #version <-ʳᵉˡ "v" + #2.
Definition make_node : val :=
(*Definition make_node : val :=
λ: [<>],
let: "n" := new [ #(Nd + 1) ] in
("n" + #version) <- #0 ;;
(for: ("i" := #0; "i" < #Nd; "i" + #1)
("n" + #data + "i") <- #0) ;;
"n".
*)
\ No newline at end of file
......@@ -219,6 +219,32 @@ Definition kvnode_prots_R t s v :=
(* Reader of the library-level protocol *)
sGPS_iSP_Reader N IP t s v γm)%I.
(* We might need to prove Persistent for this. *)
Lemma kvnode_prots_WR : forall t s v,
kvnode_prots_W t s v - kvnode_prots_R t s v.
Proof.
intros; unfold kvnode_prots_W, kvnode_prots_R.
iIntros "W".
iDestruct "W" as (L) "(% & Wv & Wd & W)".
iExists L; iSplit; [done|].
iSplit; [|iSplit].
- iDestruct "Wv" as (tv) "Wv".
iExists tv.
iApply (GPS_iSP_SWWriter_Reader _ (versionP n γm γs) with "Wv").
- unfold dataObs.
iApply (big_sepL_mono with "Wd").
iIntros (k y ?) "Wd".
iDestruct "Wd" as (ti vi) "Wd".
iExists ti, vi.
iApply (GPS_iSP_SWWriter_Reader _ (dataP n γv) with "Wd").
- by iApply sGPS_iSP_SWWriter_Reader.
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
on the component locations, which we're treating as "part of the write permission". *)
Notation F := (IP true γm). (* full interp *)
Notation F_past := (IP false γm). (* read interp *)
......
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