Skip to content

Commit

Permalink
Prove replica read
Browse files Browse the repository at this point in the history
  • Loading branch information
@yunshengtw
yunshengtw committed Nov 17, 2024
1 parent 828ab2e commit d42fd41
Show file tree
Hide file tree
Showing 6 changed files with 254 additions and 46 deletions.
22 changes: 10 additions & 12 deletions external/Goose/github_com/mit_pdos/tulip/replica.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,30 +134,28 @@ Definition Replica__logRead: val :=
Definition Replica__Read: val :=
rec: "Replica__Read" "rp" "ts" "key" :=
let: "tpl" := index.Index__GetTuple (struct.loadF Replica "idx" "rp") "key" in
let: "verfast" := tuple.Tuple__ReadVersion "tpl" "ts" in
(if: (struct.get tulip.Version "Timestamp" "verfast") = #0
then ("verfast", #true)
let: ("t1", "v1") := tuple.Tuple__ReadVersion "tpl" "ts" in
(if: "t1" = #0
then (#0, "v1", #true)
else
Mutex__Lock (struct.loadF Replica "mu" "rp");;
let: "ok" := Replica__readableKey "rp" "ts" "key" in
(if: (~ "ok")
then
Mutex__Unlock (struct.loadF Replica "mu" "rp");;
(struct.mk tulip.Version [
(#0, struct.mk tulip.Value [
], #false)
else
let: "ver" := tuple.Tuple__ReadVersion "tpl" "ts" in
(if: (struct.get tulip.Version "Timestamp" "ver") = #0
let: ("t2", "v2") := tuple.Tuple__ReadVersion "tpl" "ts" in
(if: "t2" = #0
then
Mutex__Unlock (struct.loadF Replica "mu" "rp");;
("ver", #true)
(#0, "v2", #true)
else
let: "bumped" := Replica__bumpKey "rp" "ts" "key" in
(if: "bumped"
then Replica__logRead "rp" "ts" "key"
else #());;
Replica__bumpKey "rp" "ts" "key";;
Replica__logRead "rp" "ts" "key";;
Mutex__Unlock (struct.loadF Replica "mu" "rp");;
("ver", #true)))).
("t2", "v2", #true)))).

Definition Replica__writableKey: val :=
rec: "Replica__writableKey" "rp" "ts" "key" :=
Expand Down
8 changes: 2 additions & 6 deletions external/Goose/github_com/mit_pdos/tulip/tuple.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,15 +46,11 @@ Definition Tuple__ReadVersion: val :=
let: ("ver", "slow") := findVersion "ts" (struct.loadF Tuple "vers" "tuple") in
(if: (~ "slow")
then
let: "verfast" := struct.mk tulip.Version [
"Timestamp" ::= #0;
"Value" ::= struct.get tulip.Version "Value" "ver"
] in
Mutex__Unlock (struct.loadF Tuple "mu" "tuple");;
"verfast"
(#0, struct.get tulip.Version "Value" "ver")
else
Mutex__Unlock (struct.loadF Tuple "mu" "tuple");;
"ver").
(struct.get tulip.Version "Timestamp" "ver", struct.get tulip.Version "Value" "ver")).

Definition Tuple__AppendVersion: val :=
rec: "Tuple__AppendVersion" "tuple" "ts" "value" :=
Expand Down
2 changes: 1 addition & 1 deletion src/program_proof/tulip/invariance/local_read.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ Section local_read.
| _ => False
end.

Lemma replica_inv_local_read γ gid rid clog ilog st key rts hist :
Lemma replica_inv_local_read {γ gid rid clog ilog st} key rts hist :
valid_key key ->
key_to_group key = gid ->
execute_cmds (merge_clog_ilog clog ilog) = st ->
Expand Down
12 changes: 6 additions & 6 deletions src/program_proof/tulip/program/index/index.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,20 +5,20 @@ From Goose.github_com.mit_pdos.tulip Require Import index.
Section program.
Context `{!heapGS Σ, !tulip_ghostG Σ}.

Definition is_index (idx : loc) (α : replica_names) : iProp Σ.
Definition is_index (idx : loc) (γ : tulip_names) (α : replica_names) : iProp Σ.
Admitted.

#[global]
Instance is_index_persistent idx α :
Persistent (is_index idx α).
Instance is_index_persistent idx γ α :
Persistent (is_index idx γ α).
Admitted.

Theorem wp_Index__GetTuple (idx : loc) (key : string) α :
Theorem wp_Index__GetTuple (idx : loc) (key : string) γ α :
key ∈ keys_all ->
is_index idx α -∗
is_index idx γ α -∗
{{{ True }}}
Index__GetTuple #idx #(LitString key)
{{{ (tpl : loc), RET #tpl; is_tuple tpl key α }}}.
{{{ (tpl : loc), RET #tpl; is_tuple tpl key γ α }}}.
Proof.
(*@ func (idx *Index) GetTuple(key string) *Tuple { @*)
(*@ // TODO @*)
Expand Down
220 changes: 208 additions & 12 deletions src/program_proof/tulip/program/replica/replica.v
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
From Perennial.program_proof.tulip.invariance Require Import validate execute accept learn.
From Perennial.program_proof.tulip.invariance Require Import
validate execute accept learn local_read.
From Perennial.program_proof Require Import std_proof.
From Perennial.program_proof.tulip.program Require Import prelude.
From Perennial.program_proof.tulip.program.replica Require Import
Expand Down Expand Up @@ -49,19 +50,214 @@ Section replica.
"#HtxnlogP" ∷ readonly (rp ↦[Replica :: "txnlog"] #txnlog) ∗
"#Htxnlog" ∷ is_txnlog txnlog gid γ.

Definition is_replica_idx (rp : loc) α : iProp Σ :=
Definition is_replica_idx (rp : loc) γ α : iProp Σ :=
∃ (idx : loc),
"#HidxP" ∷ readonly (rp ↦[Replica :: "idx"] #idx) ∗
"#Hidx" ∷ is_index idx α.
"#Hidx" ∷ is_index idx γ α.

Definition is_replica (rp : loc) : iProp Σ :=
∃ (mu : loc) (gid rid : u64) γ α,
Definition is_replica (rp : loc) gid rid γ : iProp Σ :=
∃ (mu : loc) α,
"#HmuP" ∷ readonly (rp ↦[Replica :: "mu"] #mu) ∗
"#Hlock" ∷ is_lock tulipNS #mu (own_replica rp gid rid γ α) ∗
"#Htxnlog" ∷ is_replica_txnlog rp gid γ ∗
"#Hidx" ∷ is_replica_idx rp α ∗
"#Hidx" ∷ is_replica_idx rp γ α ∗
"#Hinv" ∷ know_tulip_inv γ ∗
"%Hgid" ∷ ⌜gid ∈ gids_all⌝.
"%Hgid" ∷ ⌜gid ∈ gids_all⌝ ∗
"%Hrid" ∷ ⌜rid ∈ rids_all⌝.

Theorem wp_Replica__logRead (rp : loc) (ts : u64) (key : string) :
{{{ True }}}
Replica__logRead #rp #ts #(LitString key)
{{{ RET #(); True }}}.
Proof.
(*@ func (rp *Replica) logRead(ts uint64, key string) { @*)
(*@ // TODO: Create an inconsistent log entry for reading @key at @ts. @*)
(*@ } @*)
Admitted.

Theorem wp_Replica__Read (rp : loc) (tsW : u64) (key : string) gid rid γ :
let ts := uint.nat tsW in
ts ≠ O ->
key ∈ keys_all ->
key_to_group key = gid ->
is_replica rp gid rid γ -∗
{{{ True }}}
Replica__Read #rp #tsW #(LitString key)
{{{ (t : u64) (v : dbval) (ok : bool), RET (#t, dbval_to_val v, #ok);
if ok
then if decide (uint.nat t = O)
then is_repl_hist_at γ key (pred ts) v
else is_repl_hist_at γ key (uint.nat t) v ∗
read_promise γ gid rid key (uint.nat t) ts ∗
⌜(uint.nat t < pred ts)⌝
else True
}}}.
Proof.
iIntros (ts Htsnz Hkey Hkg) "#Hrp".
iIntros (Φ) "!> _ HΦ".
wp_rec.

(*@ func (rp *Replica) Read(ts uint64, key string) (uint64, tulip.Value, bool) { @*)
(*@ tpl := rp.idx.GetTuple(key) @*)
(*@ @*)
iNamed "Hrp". iNamed "Hidx".
wp_loadField.
wp_apply (wp_Index__GetTuple with "Hidx"); first apply Hkey.
iIntros (tpl) "#Htpl".

(*@ t1, v1 := tpl.ReadVersion(ts) @*)
(*@ @*)
wp_apply (wp_Tuple__ReadVersion_xphys with "Htpl").
iIntros (t1 v1) "Hread1".
wp_pures.

(*@ if t1 == 0 { @*)
(*@ // Fast-path read. @*)
(*@ return 0, v1, true @*)
(*@ } @*)
(*@ @*)
case_bool_decide as Ht1; wp_pures.
{ iApply "HΦ". by case_decide; last inv Ht1. }

(*@ rp.mu.Lock() @*)
(*@ @*)
wp_loadField.
wp_apply (wp_Mutex__Lock with "Hlock").
iIntros "[Hlocked Hrp]".

(*@ ok := rp.readableKey(ts, key) @*)
(*@ @*)
do 2 iNamed "Hrp".
wp_apply (wp_Replica__readableKey with "Hptsmsptsm"); first apply Hkey.
iIntros (ok) "[Hptsmsptsm %Hreadable]".
wp_pures.

(*@ if !ok { @*)
(*@ // Trying to read a tuple that is locked by a lower-timestamp @*)
(*@ // transaction. This read has to fail because the value to be read is @*)
(*@ // undetermined---the prepared transaction might or might not commit. @*)
(*@ rp.mu.Unlock() @*)
(*@ return 0, tulip.Value{}, false @*)
(*@ } @*)
(*@ @*)
destruct ok; wp_pures; last first.
{ wp_loadField.
wp_apply (wp_Mutex__Unlock with "[-HΦ]").
{ by iFrame "Hlock Hlocked ∗ # %". }
wp_pures.
by iApply ("HΦ" $! _ None).
}

(*@ t2, v2 := tpl.ReadVersion(ts) @*)
(*@ @*)
assert (is_Some (histm !! key)) as [hist Hhist].
{ unshelve epose proof (execute_cmds_apply_cmds cloga ilog cm histm _) as Happly.
{ by eauto 10. }
pose proof (apply_cmds_dom _ _ _ Happly) as Hdomhistm.
by rewrite -elem_of_dom Hdomhistm.
}
iDestruct (big_sepM_lookup_acc with "Hhistm") as "[Hhist HhistmC]"; first apply Hhist.
wp_apply (wp_Tuple__ReadVersion with "Htpl Hhist").
iIntros (t2 v2) "[Hhist #Hlb]".
iDestruct ("HhistmC" with "Hhist") as "Hhistm".
wp_pures.

(*@ if t2 == 0 { @*)
(*@ // Fast-path read. @*)
(*@ rp.mu.Unlock() @*)
(*@ return 0, v2, true @*)
(*@ } @*)
(*@ @*)
case_bool_decide as Ht2; wp_pures.
{ wp_loadField.
wp_apply (wp_Mutex__Unlock with "[-HΦ]").
{ by iFrame "Hlock Hlocked ∗ # %". }
wp_pures.
iApply "HΦ".
by case_decide; last inv Ht2.
}

(*@ // Slow-path read. @*)
(*@ rp.bumpKey(ts, key) @*)
(*@ @*)
wp_apply (wp_Replica__bumpKey with "Hptsmsptsm").
{ clear -Htsnz. word. }
{ apply Hkey. }
iIntros (spts) "[Hptsmsptsm %Hspts]".

(*@ // TODO: An optimization is to create a log entry iff the smallest @*)
(*@ // preparable timestamp is actually bumped, which can be checked with the @*)
(*@ // return value of @rp.bumpKey. @*)
(*@ @*)
(*@ // Logical actions: Execute() and then LocalRead(@ts, @key) @*)
(*@ rp.logRead(ts, key) @*)
(*@ @*)
wp_pures.
wp_apply wp_Replica__logRead.
iApply fupd_wp.
iInv "Hinv" as "> HinvO" "HinvC".
iNamed "HinvO".
iDestruct (big_sepS_elem_of_acc with "Hgroups") as "[Hgroup HgroupsC]"; first apply Hgid.
iDestruct (big_sepS_elem_of_acc with "Hrgs") as "[Hrg HrgsC]"; first apply Hgid.
iDestruct (big_sepS_elem_of_acc with "Hrg") as "[Hrp HrgC]"; first apply Hrid.
(* First catching up the consistent log. *)
destruct Hcloga as [cmdsa ->].
iMod (replica_inv_execute with "Hclogalb Hclog Hilog Hgroup Hrp")
as "(Hclog & Hilog & Hgroup & Hrp)".
iMod (replica_inv_local_read key ts with "Hclog Hilog Hgroup Hrp")
as "(Hclog & Hilog & Hgroup & Hrp & #Hpromise & #Hrepllb)".
{ apply Hkey. }
{ apply Hkg. }
{ apply Hexec. }
{ simpl.
rewrite /key_readable in Hreadable.
destruct (ptsm !! key) as [pts |] eqn:Hpts; rewrite Hpts in Hreadable; last done.
exists spts, pts.
do 3 (split; first done).
clear -Hreadable. word.
}
iDestruct ("HgroupsC" with "Hgroup") as "Hgroups".
iDestruct ("HrgC" with "Hrp") as "Hrg".
iDestruct ("HrgsC" with "Hrg") as "Hrgs".
iMod ("HinvC" with "[$Htxnsys $Hkeys $Hgroups $Hrgs]") as "_".
iModIntro.

(*@ rp.mu.Unlock() @*)
(*@ return t2, v2, true @*)
(*@ } @*)
wp_loadField.
wp_apply (wp_Mutex__Unlock with "[-HΦ]").
{ iFrame "Hlock Hlocked ∗ # %".
iPureIntro. simpl.
exists ptgsm.
split; first done.
split.
{ rewrite Forall_forall.
intros [n c] Hilog. simpl.
apply elem_of_app in Hilog as [Hilog | Hnewc].
{ rewrite Forall_forall in Hvicmds. by specialize (Hvicmds _ Hilog). }
rewrite elem_of_list_singleton in Hnewc.
by inv Hnewc.
}
{ rewrite merge_clog_ilog_snoc_ilog; last done.
rewrite /execute_cmds foldl_snoc execute_cmds_unfold Hexec /=.
erewrite lookup_alter_Some; last apply Hspts.
f_equal.
}
}
wp_pures.
iApply "HΦ".
case_decide as Hnz; first done.
iDestruct "Hlb" as "[Hlb' %Hv2]".
clear Ht2.
destruct Hv2 as (Hv2 & Ht2 & Hlenhist).
rewrite Ht2.
iFrame "Hrepllb Hpromise".
iPureIntro.
split.
{ by rewrite -last_lookup. }
{ clear -Ht2 Hnz Hlenhist. word. }
Qed.

Theorem wp_Replica__multiwrite rp (tsW : u64) pwrsS pwrsL pwrs histm gid γ α :
let ts := uint.nat tsW in
Expand All @@ -70,7 +266,7 @@ Section replica.
dom histm = keys_all ->
safe_extension ts pwrs histm ->
([∗ map] k ↦ h ∈ filter_group gid histm', is_repl_hist_lb γ k h) -∗
is_replica_idx rp α -∗
is_replica_idx rp γ α -∗
{{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗ own_replica_histm rp histm α }}}
Replica__multiwrite #rp #tsW (to_val pwrsS)
{{{ RET #();
Expand Down Expand Up @@ -298,7 +494,7 @@ Section replica.
valid_pwrs gid pwrs ->
group_histm_lbs_from_log γ gid cloga' -∗
is_txn_log_lb γ gid cloga' -∗
is_replica_idx rp α -∗
is_replica_idx rp γ α -∗
{{{ own_dbmap_in_slice pwrsS pwrsL pwrs ∗
own_replica_with_cloga_no_lsna rp cloga gid rid γ α
}}}
Expand Down Expand Up @@ -617,7 +813,7 @@ Section replica.
valid_ccommand gid cmd ->
group_histm_lbs_from_log γ gid cloga' -∗
is_txn_log_lb γ gid cloga' -∗
is_replica_idx rp α -∗
is_replica_idx rp γ α -∗
{{{ own_pwrs_slice pwrsS cmd ∗
own_replica_with_cloga_no_lsna rp cloga gid rid γ α
}}}
Expand Down Expand Up @@ -670,8 +866,8 @@ Section replica.
}
Qed.

Theorem wp_Replica__Start rp :
is_replica rp -∗
Theorem wp_Replica__Start rp gid rid γ :
is_replica rp gid rid γ -∗
{{{ True }}}
Replica__Start #rp
{{{ RET #(); True }}}.
Expand Down
Loading

0 comments on commit d42fd41

Please sign in to comment.