Commit d46f304e authored by William Mansky's avatar William Mansky

Finished write_all_spec and 1/3 of read_all_spec.

parent b859f3ae
......@@ -43,4 +43,4 @@ theories/examples/kvnode_code.v
theories/examples/kvnode.v
theories/examples/kvnode2.v
theories/examples/kvgroup_code.v
theories/examples/kvll_code.v
theories/examples/kvgroup.v
This diff is collapsed.
......@@ -5,7 +5,8 @@ Definition read_all : val :=
let: "snap" := !ᵃᶜ("n" + #version) in
if: "snap" `mod` #2 = #1 then "read_all" ["n"; "out"]
else (for: ("i" := #0; "i" < #Nd; "i" + #1)
read ["n"; "out" + "i"]) ;;
let: "ni" := !ᵃᶜ("n" + #data + "i") in
read ["ni"; "out" + (#Nd * "i")]) ;;
let: "v" := !ᵃᶜ("n" + #version) in
if: "v" = "snap" then # else "read_all" ["n"; "out"].
......
......@@ -191,10 +191,13 @@ End helpers.
Context (IP : interpSC Σ (nat * list Z) Prtcl).
Context (N : namespace).
Context (n : loc).
Context (γm γv: gname) (γs : list gname).
Section library_prots.
Context (n : loc).
(** 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
(* Single-Writer of version location *)
......@@ -219,8 +222,6 @@ 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.
......@@ -241,10 +242,24 @@ Proof.
- by iApply sGPS_iSP_SWWriter_Reader.
Qed.
End library_prots.
Lemma kvnode_Readers_agree : forall n1 n2 t1 t2 s1 s2 v1 v2 E, N E ->
kvnode_prots_R n1 t1 s1 v1 - kvnode_prots_R n2 t2 s2 v2 ={E}= s1 s2 t1 t2 s2 s1 t2 t1.
Proof.
intros; unfold kvnode_prots_R.
iIntros "R1 R2".
iDestruct "R1" as (??) "(_ & _ & R1)".
iDestruct "R2" as (??) "(_ & _ & R2)".
by iApply (sGPS_iSP_Readers_agree with "R1 R2").
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". *)
Context (n : loc).
Notation F := (IP true γm). (* full interp *)
Notation F_past := (IP false γm). (* read interp *)
......@@ -252,12 +267,12 @@ 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)
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') }}}
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' }}}.
kvnode_prots_W n 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? *)
......@@ -402,10 +417,9 @@ Qed.
Lemma read_spec (out: loc) t s v vals
(R Q : time Prtcl (nat * list Z) vProp) tid E
(Hlen: length vals = Nd)
(DISJ: histN ## N) (SUB1: histN E) (SUB2: N E) (SUB3: kvnodeN n E) :
{{{ ([ list] i seq O Nd, (out >> Z.of_nat i) -)
kvnode_prots_R t s (v, vals)
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'))
......@@ -414,7 +428,7 @@ Lemma read_spec (out: loc) t s v vals
read [ #n ; #out] in tid @ E
{{{ t' s' v' vals', RET #; (t t')%positive s s'⌝
([ list] ix vals', (out >> Z.of_nat i) #(LitInt x))
kvnode_prots_R t' s' (v', vals') Q t' s' (v', vals') }}}.
kvnode_prots_R n t' s' (v', vals') Q t' s' (v', vals') }}}.
Proof.
iIntros (Φ) "(out & #R & VS1 & VS2) Post".
iLöb as "IH".
......
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