Commit 2818a1b2 authored by William Mansky's avatar William Mansky

Proved Closed for kvgroup code.

parent 0206d921
......@@ -9,7 +9,7 @@ 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.
Implicit Types (L: gmap nat (list Z)) (γ: gname).
Implicit Types (L: gmap nat (list Z)) (γ: gname) (GL: gmap nat (list (list Z))).
Definition kvgroupN (n: loc) := nroot .@ "kvnodeN" .@ n.
......@@ -26,24 +26,26 @@ Qed.
Section kvnode.
Context `{!noprolG Σ,
kvprot: !gpsSimplG Σ (nat * list Z) Prtcl,
(* should the version numbers for the component kvnodes be included here? *)
kvprot: !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 : interpC Σ ghistProtocol :=
(λ _ _ _ _ s v, (z: Z) ver, v = #z log_latest s ver z t tsm,
Definition gdataP (n: loc) γv : interpSC Σ (nat * list Z) ghistProtocol :=
(λ _ _ _ s '(_, vals), log_latest s ver vals 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 l tv s v :
Persistent (dataP n γv b l γv tv s v) := _.
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:=
([ list] i↦γi γs, ti vi,
GPS_iSP_Reader (kvnodeN n) (dataP n γv) (dataP n γv false)
(n >> data >> (Z.of_nat i)) ti (map_nth i L O) vi γi)%I.
(* 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.
Definition gversionP (n: loc) γm γs : interpC Σ (versionProtocol Prtcl) :=
(λ _ _ γv _ s v, v = #(Z.of_nat s.1)
......
From gpfsl.examples Require Export kvnode_code.
Definition read_all : val :=
rec: "read_all" ["n"; "out"] :=
let: "snap" := !ᵃᶜ("n" + #version) in
Program Definition read_all : val :=
@RecV "read_all" [BNamed "n"; BNamed "out"]
(let: "snap" := !ᵃᶜ("n" + #version) in
if: "snap" `mod` #2 = #1 then "read_all" ["n"; "out"]
else (for: ("i" := #0; "i" < #Nd; "i" + #1)
"ni" <- !ᵃᶜ("n" + #data + "i");;
"read" ["ni"; "out" + (#Nd * "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"].
if: "v" = "snap" then # else "read_all" ["n"; "out"]) _.
Next Obligation.
Proof.
unfold Closed; simpl.
repeat (apply andb_prop_intro; split; [|done]).
apply is_closed_of_val.
Qed.
Definition write_all : val :=
λ: ["n"; "in"],
let: "v" := !ᵃᶜ("n" + #version) in
Program Definition write_all : val :=
@RecV <> [BNamed "n"; BNamed "in"]
(let: "v" := !ᵃᶜ("n" + #version) in
"n" + #version <-ʳᵉˡ "v" + #1 ;;
(for: ("i" := #0; "i" < #Nd; "i" + #1)
"ni" <- !ᵃᶜ("n" + #data + "i");;
"write" ["ni"; "in" + (#Nd * "i")]) ;;
"n" + #version <-ʳᵉˡ "v" + #2.
let: "ni" := !ᵃᶜ("n" + #data + "i") in
write ["ni"; "in" + (#Nd * "i")]);;
"n" + #version <-ʳᵉˡ "v" + #2) _.
Next Obligation.
Proof.
unfold Closed; simpl.
repeat (apply andb_prop_intro; split; [|done]).
apply is_closed_of_val.
Qed.
(*
(* TODO: this is split in 2 funtions because solve_closed can't work at once. *)
(* Definition make_node : val :=
λ: [<>],
......@@ -35,3 +48,4 @@ Definition init_node : val :=
"n".
Definition make_node : val :=
λ: [<>], let: "n" := new [ #(Nd + 1)] in init_node ["n"].
*)
\ No newline at end of file
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