Commit b43c1414 authored by William Mansky's avatar William Mansky

Changes based on conversation with Hai.

parent 316abd43
......@@ -207,25 +207,29 @@ Definition kvnode_IP : interpSC Σ (nat * list Z) Prtcl :=
λ b γ t s e_x,
(IP b γ t s e_x if b then kvnode_prots_W (fst e_x) (snd e_x) else kvnode_prots_R (fst e_x) (snd e_x))%I.
Notation F := (kvnode_IP true). (* full interp *)
Notation F_past := (kvnode_IP false). (* read interp *)
Notation F := ((*kvnode_*)IP true). (* full interp *)
Notation F_past := ((*kvnode_*)IP false). (* read interp *)
Definition kvget (n : nat) (v : nat * list Z) := nth n (snd v) 0.
(* Alternatively, instead of kvnode_IP, we could consider kvnode_prots_R/W to be part of the protocol-level reader/writer assertion. *)
Lemma write_spec ain tid v vals
γ s s' t Vb (E : coPset) (R : vProp)
γ s s' t (E : coPset) (R : vProp)
(Le: s s') (*(HN : physN E) (HNl: persist_locN .@ n E)*):
{{{ ([ list] i seq 0 8, (ain >> (Z.of_nat i)) LitV (kvget i vals))
sGPS_SWWriter t s v γ (monPred_in Vb sGPS_INV kvnode_IP γ)
sGPS_iSP_Writer N kvnode_IP t s v γ
<obj> (F γ t s v ={E}= F γ t s' vals R) }}}
write [ #n; #ain] in tid
{{{ t', RET #; (t < t')%positive sGPS_SWWriter t' s' vals γ
(monPred_in Vb sGPS_INV kvnode_IP γ) R }}}.
{{{ t', RET #; (t < t')%positive sGPS_iSP_Writer N kvnode_IP t' s' vals γ R }}}.
Proof.
iIntros (Φ) "(Hdata & Hshift & HP & Hinv) Hpost".
iIntros (Φ) "(Hdata & Hwrite & Hstep) Hpost".
unfold write.
wp_lam.
rewrite {1}/subst. simpl_subst. (* TODO: why do we need this? *)
wp_op. wp_bind (!ᵃᶜ_)%E.
iDestruct "node_state" as "(MS & W & HM & DO)". iDestruct "W" as (t0) "W".
(* read version, this is a single-writer read *)
wp_op. wp_bind (!ᵃᶜ_)%E. simpl.
......
......@@ -53,7 +53,7 @@ Section Interpretation.
(λ _ _ γv _ s v, v = #(Z.of_nat s)
if even s then
( L vs, map_size L Nd log_latest L s vs
hist_snapshot γh L dataObs n L γs γv t st, sGPS_SWWriter t st (s, vs) γm)
hist_snapshot γh L dataObs n L γs γv t st, sGPS_SWReader t st (s, vs) γm)
else True)%I.
Definition versionPC : interpCasC Σ natProtocol := (λ _ _ _ _ _, True)%I.
......
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