Timings for becomeleader_proof.v
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-perennial.dev/./src/program_proof/vrsm/paxos/becomeleader_proof.v.timing
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-perennial.dev/./src/program_proof/vrsm/paxos/becomeleader_proof.v.timing
From Perennial.program_proof Require Import grove_prelude.
From Goose.github_com.mit_pdos.gokv Require paxos.
From Perennial.program_proof.grove_shared Require Import urpc_proof urpc_spec.
From Perennial.goose_lang.lib Require Import waitgroup.
From iris.base_logic Require Export lib.ghost_var mono_nat.
From iris.algebra Require Import dfrac_agree mono_list.
From Perennial.goose_lang Require Import crash_borrow.
From Perennial.program_proof Require Import marshal_stateless_proof.
From Perennial Require Export paxos.definitions paxos.enternewepoch_proof.
Section becomeleader_proof.
Context `{Hparams:!paxosParams.t Σ}.
Lemma wp_Server__TryBecomeLeader s γ γsrv Ψ Φ :
is_Server s γ γsrv -∗
(Ψ -∗ Φ #()) -∗
becomeLeader_core_spec Ψ -∗
WP Server__TryBecomeLeader #s {{ Φ }}
.
wp_apply (acquire_spec with "HmuInv").
iIntros "[Hlocked Hown]".
(* already leader, no need to do anything *)
wp_apply (release_spec with "[-HΦ HΨ]").
repeat iExists _; iFrame "∗#%".
wp_apply (wp_allocStruct).
iIntros (args_ptr) "Hargs".
wp_apply (release_spec with "[-HΦ Hargs HΨ]").
repeat iExists _; iFrame "∗#%".
iIntros (numReplies_ptr) "HnumReplies".
iMod (readonly_load with "Hclerks_sl") as (?) "Hclerks_sl2".
iDestruct (own_slice_small_sz with "Hclerks_sl2") as "%Hclerks_sz".
iIntros (replies_sl) "Hreplies_sl".
set (newepoch:=word.add pst.(paxosState.epoch) 1%Z).
iMod (ghost_var_alloc ()) as (γescrow) "HreplyPostEscrow".
set (replyInv:=(
∃ (numReplies:u64) (reply_ptrs:list loc),
"%HlenEq" ∷ ⌜length reply_ptrs = length γ.(s_hosts) ⌝ ∗
"HnumReplies" ∷ numReplies_ptr ↦[uint64T] #numReplies ∗
"Hreplies_sl" ∷ own_slice_small replies_sl ptrT 1 reply_ptrs ∗
"Hreplies" ∷ (ghost_var γescrow 1 () ∨ [∗ list] i ↦ reply_ptr ; γsrv' ∈ reply_ptrs ; γ.(s_hosts),
⌜reply_ptr = null⌝ ∨ (∃ reply, (enterNewEpochReply.own reply_ptr reply 1) ∗
(if decide (reply.(enterNewEpochReply.err) = (U64 0)) then
enterNewEpoch_post γ γsrv' reply newepoch
else
True)
))
)%I).
wp_apply (newlock_spec N _ replyInv with "[HnumReplies Hreplies_sl]").
iDestruct (own_slice_to_small with "Hreplies_sl") as "$".
iDestruct (big_sepL2_length with "Hclerks_rpc") as "%Hlen".
rewrite replicate_length.
instantiate (1:=(λ _ _ _, True)%I).
by rewrite replicate_length.
rewrite lookup_replicate in H.
iIntros (muReply) "#HmuReplyInv".
wp_apply (wp_newCond with "HmuReplyInv").
iIntros (numReplies_cond) "#HnumReplies_cond".
iDestruct (struct_fields_split with "Hargs") as "HH".
iMod (readonly_alloc_1 with "epoch") as "#Hargs_epoch".
iMod (readonly_load with "Hclerks_sl") as (?) "Hclerks_sl2".
wp_apply (wp_forSlice (λ _, True%I) (V:=loc) with "[] [$Hclerks_sl2]").
iIntros (?? Φ) "!# (_ & %Hi_le & %Hi_lookup) HΦ".
wp_apply (wp_fork with "[]").
(* make applyAsFollower RPC and put reply in the replies list *)
(* establish is_singleClerk *)
iDestruct (big_sepL2_lookup_1_some with "Hclerks_rpc") as (?) "%Hi_conf_lookup".
iAssert (_) with "Hclerks_rpc" as "Hclerks_rpc2".
iDestruct (big_sepL2_lookup_acc with "Hclerks_rpc2") as "[#His_ck _]".
iMod (readonly_load with "Hargs_epoch") as (?) "Hargs_epoch2".
wp_apply (wp_singleClerk__enterNewEpoch with "[$His_ck Hargs_epoch2]").
instantiate (2:=enterNewEpochArgs.mkC newepoch).
iIntros (reply_ptr reply) "Hreply".
wp_apply (acquire_spec with "HmuReplyInv").
iIntros "[Hlocked Hown]".
pose proof (lookup_lt_Some _ _ _ Hi_conf_lookup) as Hineq.
rewrite -HlenEq in Hineq.
apply (list_lookup_lt) in Hineq.
destruct Hineq as [? Hi_replies_lookup].
wp_apply (wp_SliceSet with "[$Hreplies_sl]").
iDestruct "Hreply" as "[Hreply Hpost]".
wp_apply (wp_If_optional _ _ (True%I)).
wp_apply (wp_condSignal with "HnumReplies_cond").
(* iMod (readonly_alloc_1 with "Hreply") as "Hreply". *)
wp_apply (release_spec with "[-]").
iDestruct "Hreplies" as "[$|Hreplies]".
iDestruct (big_sepL2_insert_acc with "Hreplies") as "[_ Hreplies2]".
iDestruct ("Hreplies2" $! reply_ptr x2 with "[Hreply Hpost]") as "Hreplies3".
replace (<[int.nat i:=x2]> γ.(s_hosts)) with (γ.(s_hosts)) ; last first.
wp_apply (acquire_spec with "HmuReplyInv").
iIntros "[Hlocked Hown]".
(* continue waiting for there to be enough replies *)
wp_apply (wp_condWait with "[$HnumReplies_cond $HmuReplyInv $Hlocked Hreplies_sl Hreplies HnumReplies]").
iIntros "[Hlocked Hown]".
(* done waiting, have enough replies now *)
wp_apply (wp_ref_of_zero).
iIntros (latestReply_ptr) "HlatestReply".
iIntros (numSuccesses_ptr) "HnumSuccesses".
iDestruct "Hreplies" as "[Hbad|Hreplies]".
iDestruct (ghost_var_valid_2 with "Hbad HreplyPostEscrow") as %Hbad.
set (I:=λ (i:u64), (
∃ (W: gset nat) (latestReply_loc:loc),
"%HW_in_range" ∷ ⌜∀ s, s ∈ W → s < int.nat i⌝ ∗
"%HW_size_nooverflow" ∷ ⌜(size W) ≤ int.nat i⌝ ∗
"HnumSuccesses" ∷ numSuccesses_ptr ↦[uint64T] #(U64 (size W)) ∗
"HlatestReply_loc" ∷ latestReply_ptr ↦[ptrT] #latestReply_loc ∗
"Hreplies" ∷ ([∗ list] j ↦ reply_ptr ; γsrv' ∈ reply_ptrs ; γ.(s_hosts) ,
⌜int.nat i ≤ j⌝ →
⌜reply_ptr = null⌝ ∨ (∃ reply, (enterNewEpochReply.own reply_ptr reply 1) ∗
(if decide (reply.(enterNewEpochReply.err) = (U64 0)) then
enterNewEpoch_post γ γsrv' reply newepoch
else
True)
)) ∗
if (decide (size W = 0)) then
True
else
∃ latestReply latestLog,
"HlatestReply" ∷ (enterNewEpochReply.own latestReply_loc latestReply 1) ∗
"%Hlatestlog" ∷ ⌜latestReply.(enterNewEpochReply.state) = get_state latestLog⌝ ∗
"%HlatestlogLen" ∷ ⌜int.nat latestReply.(enterNewEpochReply.nextIndex) = length latestLog⌝ ∗
"%HlatestEpoch_ineq" ∷ ⌜int.nat latestReply.(enterNewEpochReply.acceptedEpoch) < int.nat newepoch⌝ ∗
"#Hlatest_prop" ∷ is_proposal (config:=γ.(s_hosts)) (N:=N)
γ.(s_mp) latestReply.(enterNewEpochReply.acceptedEpoch) latestLog ∗
"#HP_latest" ∷ (□ Pwf latestReply.(enterNewEpochReply.state)) ∗
"#Hacc_lbs" ∷ (□ [∗ list] s ↦ γsrv' ∈ γ.(s_hosts), ⌜s ∈ W⌝ →
is_accepted_upper_bound γsrv' latestLog
latestReply.(enterNewEpochReply.acceptedEpoch)
newepoch
) ∗
"Hvotes" ∷ ([∗ list] s ↦ γsrv' ∈ γ.(s_hosts), ⌜s ∈ W⌝ → own_vote_tok γsrv' newepoch)
)%I).
wp_apply (wp_forSlice (V:=loc) I _ _ _ _ _ reply_ptrs with "[] [HnumSuccesses HlatestReply Hreplies_sl Hreplies]").
iDestruct (big_sepL2_impl with "Hreplies []") as "$".
(* one iteration of loop *)
iIntros (?? Φ) "!# (Hi & %Hi_lt & %Hi_lookup) HΦ".
iDestruct (big_sepL2_lookup_1_some with "Hreplies") as (?) "%Hi_conf_lookup".
iDestruct (big_sepL2_lookup_acc_impl with "Hreplies") as "[Hreply_post Hreplies]".
iSpecialize ("Hreply_post" with "[% //]").
iDestruct "Hreply_post" as "[%Hbad|Hreply_post]".
iDestruct "Hreply_post" as (?) "[Hreply Hpost]".
(* got ENone, increase size of W *)
(* this is the first successful reply, no need to compare with other replies *)
replace (W) with (∅:gset nat); last first.
assert (size W = 0) as Hsz.
apply (f_equal int.Z) in Heqb3.
replace (int.Z (U64 0)) with (0%Z) in Heqb3 by word.
apply size_empty_inv in Hsz.
iExists {[ int.nat i ]}, x.
apply elem_of_singleton_1 in Hin as ->.
destruct (decide (_)); last first.
iDestruct "Hpost" as (?) "(%Hepoch_ineq & %Hlog & %Hlen & #Hacc_ub & #Hprop & #HP2 & Hvote)".
iIntros (??????) "Hwand".
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) in * by word.
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) in * by word.
iSplitR "Hvote"; last first.
iDestruct (big_sepL_lookup_acc_impl with "[]") as "[_ Hwand]".
iApply ("Hwand" with "[] [Hvote]").
rewrite elem_of_singleton in H2.
replace (x0) with (x2); last first.
apply elem_of_singleton_1 in H0.
rewrite H in Hi_conf_lookup.
by injection Hi_conf_lookup.
(* In this case, there have been previous successful replies. Compare with latestReply *)
destruct (decide (size W = 0)).
iRename "Hreply_acceptedEpoch" into "Hreply_acceptedEpoch2".
iRename "Hreply_nextIndex" into "Hreply_nextIndex2".
iDestruct "Hreply_err" as "?".
iDestruct "Hreply_ret" as "?".
iDestruct "Hreply_ret_sl" as "?".
(* case: newreply.acceptedEpoch > latestReply.acceptedEpoch *)
iExists (W ∪ {[ int.nat i ]}), x.
apply elem_of_union in H as [H|H].
specialize (HW_in_range s0 H).
rewrite elem_of_singleton in H.
rewrite size_union; last first.
apply disjoint_singleton_r.
destruct (decide (int.nat i ∈ W)).
specialize (HW_in_range (int.nat i) e).
replace (word.add (size W) 1) with (U64 (size W + 1)%nat) by word.
iIntros (??????) "Hwand".
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) in H2 by word.
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) in H by word.
destruct (decide (size W + 1 = 0)).
destruct (decide (_)); last first.
iDestruct "Hpost" as (?) "(%Hepoch_ineq & %Hlog & %Hlen & #Hacc_ub & #Hprop & #HP2 & Hvote)".
iSplitR "Hvote Hvotes Hprop".
repeat iExists _; iFrame "∗#".
iSplitR "Hvotes Hvote"; last first.
iDestruct (big_sepL_lookup_acc_impl with "Hvotes") as "[_ Hwand]".
iApply ("Hwand" with "[] [Hvote]").
rewrite elem_of_union in Hk.
destruct Hk as [Hk|Hbad].
rewrite elem_of_singleton in Hbad.
iApply (big_sepL_impl with "Hacc_lbs").
rewrite elem_of_union in Hin.
destruct Hin as [Hold|Hnew].
iSpecialize ("Hwand" with "[%//]").
iDestruct (is_accepted_upper_bound_mono_epoch with "Hwand") as "Hwand2".
instantiate (1:=reply.(enterNewEpochReply.acceptedEpoch)).
iDestruct (is_accepted_upper_bound_mono_log with "Hwand2") as "$".
rewrite elem_of_singleton in Hnew.
rewrite H in Hi_conf_lookup.
by injection Hi_conf_lookup.
destruct (bool_decide _) as [] eqn:X.
(* reply has higher nextIndex than latestReply *)
(* establish loop invariant *)
iExists (W ∪ {[ int.nat i ]}), x.
apply elem_of_union in H as [H|H].
specialize (HW_in_range s0 H).
rewrite elem_of_singleton in H.
rewrite size_union; last first.
apply disjoint_singleton_r.
destruct (decide (int.nat i ∈ W)).
specialize (HW_in_range (int.nat i) e).
replace (word.add (size W) 1) with (U64 (size W + 1)%nat) by word.
iIntros (??????) "Hwand".
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) in H2 by word.
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) in H by word.
destruct (decide (size W + 1 = 0)).
destruct (decide (_)); last first.
iDestruct "Hpost" as (?) "(%Hepoch_ineq & %Hlog & %Hlen & #Hacc_ub & #Hprop & #HP2 & Hvote)".
(* XXX: copy/paste votes *)
iSplitR "Hvotes Hvote"; last first.
iDestruct (big_sepL_lookup_acc_impl with "Hvotes") as "[_ Hwand]".
iApply ("Hwand" with "[] [Hvote]").
rewrite elem_of_union in Hk.
destruct Hk as [Hk|Hbad].
rewrite elem_of_singleton in Hbad.
iApply (big_sepL_impl with "Hacc_lbs").
rewrite elem_of_union in Hin.
destruct Hin as [Hold|Hnew].
iSpecialize ("Hwand" with "[%//]").
iDestruct (is_proposal_compare with "Hprop Hlatest_prop") as "%Hpre".
iDestruct (is_accepted_upper_bound_mono_log with "Hwand") as "$".
rewrite elem_of_singleton in Hnew.
rewrite H in Hi_conf_lookup.
by injection Hi_conf_lookup.
(* keep the old latestReply *)
(* establish loop invariant *)
iExists (W ∪ {[ int.nat i ]}), _.
apply elem_of_union in H as [H|H].
specialize (HW_in_range s0 H).
rewrite elem_of_singleton in H.
rewrite size_union; last first.
apply disjoint_singleton_r.
destruct (decide (int.nat i ∈ W)).
specialize (HW_in_range (int.nat i) e).
replace (word.add (size W) 1) with (U64 (size W + 1)%nat) by word.
iIntros (??????) "Hwand".
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) in H2 by word.
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) in H by word.
destruct (decide (size W + 1 = 0)).
instantiate (1:=enterNewEpochReply.mkC _ _ _ _).
destruct (decide (_)); last first.
iDestruct "Hpost" as (?) "(%Hepoch_ineq & %Hlog & %Hlen & #Hacc_ub & #Hprop & #HP2 & Hvote)".
(* XXX: copy/paste votes *)
iSplitR "Hvotes Hvote"; last first.
iDestruct (big_sepL_lookup_acc_impl with "Hvotes") as "[_ Hwand]".
iApply ("Hwand" with "[] [Hvote]").
rewrite elem_of_union in Hk.
destruct Hk as [Hk|Hbad].
rewrite elem_of_singleton in Hbad.
iApply (big_sepL_impl with "Hacc_lbs").
rewrite elem_of_union in Hin.
destruct Hin as [Hold|Hnew].
iSpecialize ("Hwand" with "[%//]").
rewrite elem_of_singleton in Hnew.
iDestruct (is_proposal_compare with "Hlatest_prop Hprop") as %Hpre.
iDestruct (is_accepted_upper_bound_mono_log with "Hacc_ub") as "$".
rewrite H in Hi_conf_lookup.
by injection Hi_conf_lookup.
(* case: epoch is not the same, so keep the old latest reply *)
(* establish loop invariant *)
iExists (W ∪ {[ int.nat i ]}), _.
apply elem_of_union in H as [H|H].
specialize (HW_in_range s0 H).
rewrite elem_of_singleton in H.
rewrite size_union; last first.
apply disjoint_singleton_r.
destruct (decide (int.nat i ∈ W)).
specialize (HW_in_range (int.nat i) e).
replace (word.add (size W) 1) with (U64 (size W + 1)%nat) by word.
iIntros (??????) "Hwand".
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) in H2 by word.
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) in H by word.
destruct (decide (size W + 1 = 0)).
iExists _, _; iFrame "#%".
destruct (decide (_)); last first.
iDestruct "Hpost" as (?) "(%Hepoch_ineq & %Hlog & %Hlen & #Hacc_ub & #Hprop & #HP2 & Hvote)".
(* XXX: copy/paste votes *)
iSplitR "Hvotes Hvote"; last first.
iDestruct (big_sepL_lookup_acc_impl with "Hvotes") as "[_ Hwand]".
iApply ("Hwand" with "[] [Hvote]").
rewrite elem_of_union in Hk.
destruct Hk as [Hk|Hbad].
rewrite elem_of_singleton in Hbad.
iApply (big_sepL_impl with "Hacc_lbs").
rewrite elem_of_union in Hin.
destruct Hin as [Hold|Hnew].
iSpecialize ("Hwand" with "[%//]").
rewrite elem_of_singleton in Hnew.
rewrite bool_decide_eq_false in X.
iDestruct (is_accepted_upper_bound_mono_epoch with "Hacc_ub") as "Hacc_ub2".
instantiate (1:=latestReply.(enterNewEpochReply.acceptedEpoch)).
destruct (decide (int.nat reply.(enterNewEpochReply.acceptedEpoch) = int.nat latestReply.(enterNewEpochReply.acceptedEpoch))).
replace (reply.(enterNewEpochReply.acceptedEpoch)) with (latestReply.(enterNewEpochReply.acceptedEpoch)) in X by word.
iDestruct (is_accepted_upper_bound_mono_log with "Hacc_ub2") as "$".
rewrite H in Hi_conf_lookup.
by injection Hi_conf_lookup.
(* got error, don't change anything *)
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) by word.
specialize (HW_in_range s0 H).
iIntros (??????) "Hwand".
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) in H2 by word.
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) in H by word.
(* null pointer, don't do anything *)
replace (int.nat (word.add i 1%Z)) with (int.nat i + 1) by word.
specialize (HW_in_range s0 H).
iApply (big_sepL2_impl with "Hreplies").
iIntros "[Hi Hreplies_sl]".
(* case: got enough replies to become leader *)
destruct (decide (size W = 0)).
replace (int.Z (word.mul 2%Z 0%nat)) with (0)%Z in Heqb1; last first.
wp_apply (wp_Server__withLock with "[]").
iRename "HP" into "HP_in".
(* case: server has not advanced past newepoch, we become leader *)
iDestruct (own_slice_small_sz with "Hreplies_sl") as "%Hreplies_sz".
instantiate (1:=paxosState.mk _ _ _ _ _).
(* start ghost reasoning *)
(* A few protocol steps *)
iMod (fupd_mask_subseteq (↑sysN)) as "Hmask".
iDestruct (big_sepL2_length with "[$Hclerks_rpc]") as %Hlen.
iMod (become_leader with "Hvote_inv Hacc_lbs Hlatest_prop Hvotes") as "HghostLeader".
enough (int.Z (word.mul 2 (size W)) <= (2 * size W))%Z.
rewrite word.unsigned_mul.
iDestruct (ghost_replica_helper1 with "Hghost") as %Hineq.
iMod (ghost_replica_leader_init with "HghostLeader Hghost") as "[Hghost Hleader]".
iSplitR "HΦ HΨ Hlocked Hreplies_sl HnumReplies Hreplies HreplyPostEscrow".
wp_apply (release_spec with "[-HΦ HΨ]").
iFrame "HmuReplyInv Hlocked".
instantiate (1:=paxosState.mk _ _ _ _ _).
Opaque own_paxosState_ghost.
Transparent own_paxosState_ghost.
wp_apply (release_spec with "[-HΦ HΨ]").
iFrame "HmuReplyInv Hlocked".
(* case: not enough replies *)
wp_apply (release_spec with "[-HΦ HΨ]").
iFrame "HmuReplyInv Hlocked".