Commit 93205e82 authored by William Mansky's avatar William Mansky

Tweaked approach to pointer protocol.

parent e864e9c5
......@@ -65,8 +65,8 @@ Section definitions.
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.
(*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.
......@@ -216,9 +216,10 @@ Definition kvgroup_prots_W t s 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,
([ list] i↦γi γs, ti (li : loc) γm' γv' γs' vi,
GPS_iSP_Writer (kvgroupN n) (ptrP n γv) (ptrP n γv false) (n >> data >> i)
ti (map_nth i GL []) vi γi)
ti (map_nth i GL []) #li γi
kvnode_prots_W (gdataP n γv) (kvgroupN n) li γm' γv' γs' ti (map_nth i GL []) vi)
(* Single-Writer of the library-level protocol *)
sGPS_iSP_Writer N IP t s v γm)%I.
......@@ -287,13 +288,17 @@ Proof.
(* loop invariant *)
set φ : Z vProp :=
(λ i : Z, 0 i Nd
([ list] ix take (Z.to_nat i) vals', ti vi γi, ⌜γs !! i = Some γi
([ list] ix take (Z.to_nat i) vals', ti (li : loc) γm' γv' γs' vi γi, ⌜γs !! i = Some γ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)
(n >> data >> i) ti (<[(v + 2)%nat := x]>(map_nth i GL [])) #li γi
kvnode_prots_W (gdataP n γv) (kvgroupN n) li γm' γv' γs' ti
(<[(v + 2)%nat := x]>(map_nth i GL [])) vi)
([ list] i seq (Z.to_nat i) (8 - Z.to_nat i),
( ti vi γi, ⌜γs !! i = Some γi
( ti (li : loc) γm' γv' γs' vi γi, ⌜γs !! i = Some γ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))
(n >> data >> Z.of_nat i) ti (map_nth i GL []) #li γi
kvnode_prots_W (gdataP n γv) (kvgroupN n) li γm' γv' γs' ti
(map_nth i GL []) vi))
([ 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 *)
......@@ -307,12 +312,18 @@ Proof.
{ 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].
iDestruct "Hi" as (ti li γm' γv' γs' vi γi Eqγi) "[Wi KVi]". 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.
destruct (lookup_lt_is_Some_2 vals' (Z.to_nat i)) as [vi Eqi].
{ rewrite Hlen Nat2Z.inj_lt Z2Nat.id; lia. }
iDestruct (big_sepL_lookup_acc _ _ _ _ Eqi with "in") as "[ini inC]".
rewrite Z2Nat.id; [|lia].
wp_read. iDestruct ("inC" with "ini") as "in".
iApply (write_spec with "KVi").
Check write_spec.
......
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