Commit 0cebeccf authored by William Mansky's avatar William Mansky

New attempt at ptr protocol for kvgroup.

parent 3af2e1f6
......@@ -7,9 +7,9 @@ From gpfsl.base_logic Require Import na list_lemmas.
From gpfsl.logic Require Export lifting proofmode logically_atomic.
From gpfsl.logic Require Import new_delete for_loop obj_invariants.
From gpfsl.gps Require Import surface protocols simpl_model.
From gpfsl.examples Require Import kvnode_helpers kvgroup_code kvnode2.
From gpfsl.examples Require Import snapshot kvnode_helpers kvgroup_code kvnode2.
Implicit Types (L: gmap nat (list Z)) (γ: gname) (GL: gmap nat (list (list Z))).
Implicit Types (L: gmap nat (list Z)) (γ: gname) (GL: gmap nat (list (list Z))) (PL: gmap nat (loc * gmap nat (list Z))).
Definition kvgroupN (n: loc) := nroot .@ "kvnodeN" .@ n.
......@@ -26,6 +26,11 @@ Proof.
Qed.
*)
Canonical Structure ptrProtocol : protocolT :=
Build_protocolT (gmap nat (loc * gmap nat (list Z))) _ _ _ map_subseteq _.
Definition historyR := snapR (gmapUR nat (agreeR (prodC (discreteC loc) (gmapC nat (listC ZC))))).
Section kvnode.
Context `{!noprolG Σ,
kvprot: !gpsSimplG Σ (nat * list Z) ghistProtocol,
......@@ -34,50 +39,59 @@ Context `{!noprolG Σ,
gpGv: !gpsG Σ (versionProtocol ghistProtocol),
gpGd: !gpsG Σ histProtocol,
gpGv': !gpsG Σ (versionProtocol Prtcl),
gpGp: !gpsG Σ ghistProtocol}.
gpGp: !gpsG Σ ptrProtocol,
histG : inG Σ historyR }.
Local Notation vProp := (vProp Σ).
Section definitions.
Definition gdataP (n: loc) γv : interpSC Σ (nat * list Z) ghistProtocol :=
(λ _ _ _ s v, ver, log_latest s ver v.2 t tsm,
Definition hist_snapshot γh PL : vProp :=
own γh (# (to_agree <$> PL) : historyR)%I.
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,
GPS_SWReader (Prtcl:=(versionProtocol Prtcl)) (n >> version) t
((ver - 1)%nat, tsm) #(ver - 1)%nat γv)%I.
Global Instance gdataP_persistent n γv b l tv s v :
Persistent (gdataP n γv b l tv s v) := _.
Global Instance gdataP_persistent n γv γh b l tv s v :
Persistent (gdataP n γv γh b l tv s v) := _.
Definition ptrP (n: loc) γv γm' γv' γs' : interpC Σ ghistProtocol :=
(λ b _ _ _ s v, p ti vi , 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 n γv) (kvgroupN n) γm' γv' γs' p ti s vi)%I.
(* This needs to be able to tell a reader that any reads from previous pointers are included in this pointer's current history. *)
Definition ptrP (n: loc) γv γm' γv' γs' γh : interpC Σ ptrProtocol :=
(λ b _ _ _ s v, p ti vi ver L PL, v = #(LitLoc p) /\ log_latest s ver (p, L) /\ map_subseteq s PL /\
forall ver' p' L', (ver' > ver)%nat -> PL !! ver' = Some (p', L') -> p' = p
(if b then hist_master 1 γh PL else hist_snapshot γh PL)
kvnode_prots_R (gdataP n γv γh) (kvgroupN n) γm' γv' γs' p ti L vi)%I.
Definition gdataObs (n: loc) GL γs γv :=
Definition gdataObs (n: loc) GL γs γv γh :=
([ list] ix γs, ti1 ti2 (li : loc) si vi, let '(γi, (γm', γv', γs')) := x in
GPS_iSP_Reader (kvgroupN n) (ptrP n γv γm' γv' γs') (ptrP n γv γm' γv' γs' false) (n >> data >> i) ti1 si #li γi
kvnode_prots_R (gdataP n γv) (kvgroupN n) γm' γv' γs' li ti2 (map_nth i GL []) vi)%I.
PL pver L0 pver' L', log_latest si pver (li, L0) /\ log_latest PL pver' (li, L') /\ log_latest L' vi.1 vi.2 hist_snapshot γh PL
GPS_iSP_Reader (kvgroupN n) (ptrP n γv γm' γv' γs' γh) (ptrP n γv γm' γv' γs' γh false) (n >> data >> i) ti1 si #li γi
kvnode_prots_R (gdataP n γv γh) (kvgroupN n) γm' γv' γs' li ti2 (map_nth i GL []) vi)%I.
Global Instance gdataObs_persistent n GL γs γv :
Persistent (gdataObs n GL γs γv).
Global Instance gdataObs_persistent n GL γs γv γh :
Persistent (gdataObs n GL γs γv γh).
Proof.
unfold gdataObs.
apply big_sepL_persistent; intros ? (?, ((?, ?), ?)); apply _.
Qed.
Definition gversionP (n: loc) γm γs : interpC Σ (versionProtocol Prtcl) :=
Definition gversionP (n: loc) γm γs γh : interpC Σ (versionProtocol Prtcl) :=
(λ _ _ γv _ s v, v = #(Z.of_nat s.1)
if even s.1 then
( GL vs, map_size GL Nd log_latest GL s.1 vs
(* observation of the data locations *)
gdataObs n GL γs γv
gdataObs n GL γs γv γh
(* observation of the library-level value *)
(sGPS_SWReader (Prtcl:=Prtcl) s.2.1 s.2.2 (s.1, vs) γm))
else True)%I.
End definitions.
Instance gversionP_persistent n γm γs b l γv tv s v :
Persistent (gversionP n γm γs b l γv tv s v).
Instance gversionP_persistent n γm γs b l γv γh tv s v :
Persistent (gversionP n γm γs b l γv γh tv s v).
Proof. apply bi.sep_persistent; [apply _|]. case (even s.1); apply _. Qed.
Section helpers.
......@@ -515,7 +529,7 @@ Proof.
|..].
{ iIntros (????) "!> !>". iSplit. by iIntros "#$". iSplit; by iIntros "#$". }
iIntros (t' s' p) "!> (% & Ri & KVi)". wp_let.
iDestruct "KVi" as (ni ? (?, ?)) "[% KVi]"; subst p.
iDestruct "KVi" as (ni ? (?, ?) ? L) "[(% & % & %) KVi]"; subst p.
(* reading *)
iDestruct (gdataObs_get_1 n GL1 γs γv (Z.to_nat i) with "DO'")
as (γi' ti1' ti2 li' si vi) "[Hγi Hdi]".
......@@ -524,6 +538,7 @@ Proof.
rewrite H in Hγi; inversion Hγi; subst γi'.
iDestruct "Hdi" as "[_ Hdi]".
wp_op. wp_op.
(* Two cases: location is the same, or KVi is more up-to-date than Hdi. *)
iApply (read_spec (gdataP n γv) (kvgroupN n) _ _ _ _ _ _ _ _ _ (fun t s v => gdataP n γv false γm' t s v)%I (fun t s v => gdataP n γv false γm' t s 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, but might also have a more up-to-date log. Do we need to reconcile them? *)
......
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