From 4c7bdfa70ad3fd4bd77d9a116747d0f542da1152 Mon Sep 17 00:00:00 2001 From: Arseny Sher Date: Wed, 27 Nov 2024 14:19:43 +0300 Subject: [PATCH] becomeleader --- safekeeper/spec/ProposerAcceptorReconfig.tla | 26 +++++++++- safekeeper/spec/ProposerAcceptorStatic.tla | 54 +++++++++++--------- 2 files changed, 54 insertions(+), 26 deletions(-) diff --git a/safekeeper/spec/ProposerAcceptorReconfig.tla b/safekeeper/spec/ProposerAcceptorReconfig.tla index 4a9b459024..d44e1d3a59 100644 --- a/safekeeper/spec/ProposerAcceptorReconfig.tla +++ b/safekeeper/spec/ProposerAcceptorReconfig.tla @@ -26,6 +26,19 @@ CONSTANT NULL \* use here and mostly create own versions of them) it doesn't. PAS == INSTANCE ProposerAcceptorStatic +\******************************************************************************** +\* Helpers +\******************************************************************************** + +\* Does set of acceptors acc_set form the quorum in the member set members? +Quorum(acc_set, members) == + LET acc_set_in_members == {a \in acc_set: a \in members} IN + Cardinality(acc_set_in_members) >= (Cardinality(members) \div 2 + 1) + +\******************************************************************************** +\* Type assertion +\******************************************************************************** + \* Is c a valid config? IsConfig(c) == /\ DOMAIN c = {"generation", "members", "newMembers"} @@ -79,6 +92,17 @@ Vote(p, a) == /\ PAS!Vote(p, a) /\ UNCHANGED <> +\* Proposer p gets elected. +BecomeLeader(p) == + /\ prop_state[p].state = "campaign" + /\ prop_conf[p] /= NULL + \* Votes must form quorum in both sets (if the newMembers exists). + /\ Quorum(DOMAIN prop_state[p].votes, prop_conf[p].members) + /\ \/ prop_conf[p].newMembers = NULL + \/ (prop_conf[p].newMembers /= NULL) /\ (Quorum(DOMAIN prop_state[p].votes, prop_conf[p].newMembers)) + /\ PAS!DoBecomeLeader(p) + /\ UNCHANGED <> + \* Do CAS on the conf store, starting change into the new_members conf. StartChange(new_members) == \* Possible only if we don't already have the change in progress. @@ -116,7 +140,7 @@ Next == \/ \E p \in proposers: RestartProposer(p) \/ \E p \in proposers: \E a \in acceptors: ProposerBumpConf(p, a) \/ \E p \in proposers: \E a \in acceptors: Vote(p, a) -\* \/ \E p \in proposers: BecomeLeader(p) + \/ \E p \in proposers: BecomeLeader(p) \* \/ \E p \in proposers: \E a \in acceptors: UpdateTerm(p, a) \* \/ \E p \in proposers: \E a \in acceptors: TruncateWal(p, a) \* \/ \E p \in proposers: NewEntry(p) diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla index e916440eb2..37c6380112 100644 --- a/safekeeper/spec/ProposerAcceptorStatic.tla +++ b/safekeeper/spec/ProposerAcceptorStatic.tla @@ -233,35 +233,39 @@ Vote(p, a) == \* Get lastLogTerm from term history th. LastLogTerm(th) == th[Len(th)].term +\* 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) + 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 + \* We copy all log preceding proposer's term from the max vote node so + \* make sure it is still on one term with us. This is a model + \* simplification which can be removed, in impl we fetch WAL on demand + \* from safekeeper which has it later. Note though that in case of on + \* demand fetch we must check on donor not only term match, but that + \* truncate_wal had already been done (if it is not max_vote_acc). + /\ acc_state[max_vote_acc].term = prop_state[p].term + /\ prop_state' = [prop_state EXCEPT ![p].state = "leader", + ![p].termHistory = prop_th, + ![p].wal = acc_state[max_vote_acc].wal + ] + /\ elected_history' = Upsert(elected_history, prop_state[p].term, 1, LAMBDA c: c + 1) + /\ UNCHANGED <> + \* Proposer p gets elected. BecomeLeader(p) == /\ prop_state[p].state = "campaign" /\ Quorum(DOMAIN prop_state[p].votes) - /\ 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) - 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 - \* We copy all log preceding proposer's term from the max vote node so - \* make sure it is still on one term with us. This is a model - \* simplification which can be removed, in impl we fetch WAL on demand - \* from safekeeper which has it later. Note though that in case of on - \* demand fetch we must check on donor not only term match, but that - \* truncate_wal had already been done (if it is not max_vote_acc). - /\ acc_state[max_vote_acc].term = prop_state[p].term - /\ prop_state' = [prop_state EXCEPT ![p].state = "leader", - ![p].termHistory = prop_th, - ![p].wal = acc_state[max_vote_acc].wal - ] - /\ elected_history' = Upsert(elected_history, prop_state[p].term, 1, LAMBDA c: c + 1) - /\ UNCHANGED <> - + /\ DoBecomeLeader(p) \* Acceptor a learns about elected proposer p's term. In impl it matches to \* VoteRequest/VoteResponse exchange when leader is already elected and is not