From cb1ebedc9fef6af2429b768bdbe70d57683a34c9 Mon Sep 17 00:00:00 2001 From: Arseny Sher Date: Fri, 29 Nov 2024 16:32:08 +0300 Subject: [PATCH] FinishChange --- safekeeper/spec/ProposerAcceptorReconfig.tla | 37 ++++++++++++++++++++ safekeeper/spec/ProposerAcceptorStatic.tla | 31 ++++++++++++---- 2 files changed, 62 insertions(+), 6 deletions(-) diff --git a/safekeeper/spec/ProposerAcceptorReconfig.tla b/safekeeper/spec/ProposerAcceptorReconfig.tla index f810ac4235..f647ad3c83 100644 --- a/safekeeper/spec/ProposerAcceptorReconfig.tla +++ b/safekeeper/spec/ProposerAcceptorReconfig.tla @@ -171,6 +171,42 @@ StartChange(new_members) == /\ conf_store' = [generation |-> conf_store.generation + 1, members |-> conf_store.members, newMembers |-> new_members] /\ UNCHANGED <> +\* Acceptor's last_log_term. +AccLastLogTerm(acc) == + PAS!LastLogTerm(PAS!AcceptorTermHistory(acc)) + +\* Do CAS on the conf store, transferring joint conf into the newMembers only. +FinishChange == + \* have joint conf + /\ conf_store.newMembers /= NULL + \* The conditions for finishing the change are: + /\ \E qo \in PAS!AllMinQuorums(conf_store.members): + \* 1) Old majority must be aware of the joint conf. + /\ \A a \in qo: conf_store.generation = acc_conf[a].generation + \* 2) New member set must have log synced, i.e. some majority needs + \* to have at least as high as max of some + \* old majority. + \* 3) Term must be synced, i.e. some majority of the new set must + \* have term >= than max term of some old majority. + \* This ensures that two leaders are never elected with the same + \* term even after config change (which would be bad unless we treat + \* generation as a part of term which we don't). + \* 4) A majority of the new set must be aware of the joint conf. + \* This allows to safely destoy acceptor state if it is not a + \* member of its current conf (which is useful for cleanup after + \* migration as well as for aborts). + /\ LET sync_pos == PAS!MaxTermLsn({[term |-> AccLastLogTerm(a), lsn |-> PAS!FlushLsn(a)]: a \in qo}) + sync_term == PAS!Maximum({acc_state[a].term: a \in qo}) + IN + \E qn \in PAS!AllMinQuorums(conf_store.newMembers): + \A a \in qn: + /\ PAS!TermLsnGE([term |-> AccLastLogTerm(a), lsn |-> PAS!FlushLsn(a)], sync_pos) + /\ acc_state[a].term >= sync_term + /\ conf_store.generation = acc_conf[a].generation + /\ conf_store' = [generation |-> conf_store.generation + 1, members |-> conf_store.newMembers, newMembers |-> NULL] + /\ UNCHANGED <> + + \******************************************************************************* \* Final spec \******************************************************************************* @@ -186,6 +222,7 @@ Next == \/ \E p \in proposers: CommitEntries(p) \/ \E p \in proposers: \E a \in acceptors: ProposerBumpConf(p, a) \/ \E new_members \in SUBSET acceptors: StartChange(new_members) + \/ FinishChange Spec == Init /\ [][Next]_<> diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla index b78a31bd87..8df33cba40 100644 --- a/safekeeper/spec/ProposerAcceptorStatic.tla +++ b/safekeeper/spec/ProposerAcceptorStatic.tla @@ -224,7 +224,16 @@ RestartProposer(p) == RestartProposerWithTerm(p, new_term) \* Term history of acceptor a's WAL: the one saved truncated to contain only <= -\* local FlushLsn entries. +\* local FlushLsn entries. Note that FlushLsn is the end LSN of the last entry +\* (and begin LSN of the next). The mental model for non strict comparison is +\* that once proposer is elected it immediately writes log record with zero +\* length. This allows leader to commit existing log without writing any new +\* entries. For example, assume acceptor has WAL +\* 1.1, 1.2 +\* written by prop with term 1; its current +\* is <1, 3>. Now prop with term 2 and max vote from this acc is elected. +\* Once TruncateWAL is done, becomes <2, 3> +\* without any new records explicitly written. AcceptorTermHistory(a) == SelectSeq(acc_state[a].termHistory, LAMBDA th_entry: th_entry.lsn <= FlushLsn(a)) @@ -243,17 +252,27 @@ Vote(p, a) == \* Get lastLogTerm from term history th. LastLogTerm(th) == th[Len(th)].term +\* Compares pairs: returns true if tl1 >= tl2. +TermLsnGE(tl1, tl2) == + /\ tl1.term >= tl2.term + /\ (tl1.term = tl2.term => tl1.lsn >= tl2.lsn) + +\* Choose max pair in the non empty set of them. +MaxTermLsn(term_lsn_set) == + CHOOSE max_tl \in term_lsn_set: \A tl \in term_lsn_set: TermLsnGE(max_tl, tl) + \* Workhorse for BecomeLeader. \* Assumes the check prop_state[p] votes is quorum has been done *outside*. DoBecomeLeader(p) == LET \* Find acceptor with the highest vote. max_vote_acc == - CHOOSE a \in DOMAIN prop_state[p].votes: - LET v == prop_state[p].votes[a] - IN \A v2 \in Range(prop_state[p].votes): - /\ LastLogTerm(v.termHistory) >= LastLogTerm(v2.termHistory) - /\ (LastLogTerm(v.termHistory) = LastLogTerm(v2.termHistory) => v.flushLsn >= v2.flushLsn) + CHOOSE a \in DOMAIN prop_state[p].votes: + LET a_vote == prop_state[p].votes[a] + a_vote_term_lsn == [term |-> LastLogTerm(a_vote.termHistory), lsn |-> a_vote.flushLsn] + vote_term_lsns == {[term |-> LastLogTerm(v.termHistory), lsn |-> v.flushLsn]: v \in Range(prop_state[p].votes)} + IN + a_vote_term_lsn = MaxTermLsn(vote_term_lsns) max_vote == prop_state[p].votes[max_vote_acc] prop_th == Append(max_vote.termHistory, [term |-> prop_state[p].term, lsn |-> max_vote.flushLsn]) IN