From 942ff3a4f6858de3a6c5e72c5ed6e7c752035f86 Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Fri, 10 Nov 2023 11:05:39 +0000 Subject: [PATCH] Align leadership state naming with implementation (#5823) --- tla/consensus/MCccfraft.cfg | 2 +- tla/consensus/MCccfraftAtomicReconfig.cfg | 2 +- tla/consensus/MCccfraftWithReconfig.cfg | 2 +- tla/consensus/SIMCoverageccfraft.cfg | 2 +- tla/consensus/SIMccfraft.cfg | 2 +- tla/consensus/Traceccfraft.cfg | 2 +- tla/consensus/Traceccfraft.tla | 8 ++--- tla/consensus/ccfraft.tla | 36 +++++++++++------------ 8 files changed, 27 insertions(+), 29 deletions(-) diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg index 5602cd0ed89d..db57df0718b6 100644 --- a/tla/consensus/MCccfraft.cfg +++ b/tla/consensus/MCccfraft.cfg @@ -23,7 +23,7 @@ CONSTANTS Candidate = Candidate Leader = Leader RetiredLeader = RetiredLeader - Pending = Pending + None = None RequestVoteRequest = RequestVoteRequest RequestVoteResponse = RequestVoteResponse diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg index 914b0e160935..64f27fbfcade 100644 --- a/tla/consensus/MCccfraftAtomicReconfig.cfg +++ b/tla/consensus/MCccfraftAtomicReconfig.cfg @@ -23,7 +23,7 @@ CONSTANTS Candidate = Candidate Leader = Leader RetiredLeader = RetiredLeader - Pending = Pending + None = None RequestVoteRequest = RequestVoteRequest RequestVoteResponse = RequestVoteResponse diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg index f6890893c8b0..21663b2df412 100644 --- a/tla/consensus/MCccfraftWithReconfig.cfg +++ b/tla/consensus/MCccfraftWithReconfig.cfg @@ -23,7 +23,7 @@ CONSTANTS Candidate = Candidate Leader = Leader RetiredLeader = RetiredLeader - Pending = Pending + None = None RequestVoteRequest = RequestVoteRequest RequestVoteResponse = RequestVoteResponse diff --git a/tla/consensus/SIMCoverageccfraft.cfg b/tla/consensus/SIMCoverageccfraft.cfg index 326dd390e73c..4c204ee17962 100644 --- a/tla/consensus/SIMCoverageccfraft.cfg +++ b/tla/consensus/SIMCoverageccfraft.cfg @@ -9,7 +9,7 @@ CONSTANTS Candidate = Candidate Leader = Leader RetiredLeader = RetiredLeader - Pending = Pending + None = None RequestVoteRequest = RequestVoteRequest RequestVoteResponse = RequestVoteResponse diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg index a61bc3a863bd..9f82642d1841 100644 --- a/tla/consensus/SIMccfraft.cfg +++ b/tla/consensus/SIMccfraft.cfg @@ -9,7 +9,7 @@ CONSTANTS Candidate = Candidate Leader = Leader RetiredLeader = RetiredLeader - Pending = Pending + None = None RequestVoteRequest = RequestVoteRequest RequestVoteResponse = RequestVoteResponse diff --git a/tla/consensus/Traceccfraft.cfg b/tla/consensus/Traceccfraft.cfg index efae38009fec..762e51385b46 100644 --- a/tla/consensus/Traceccfraft.cfg +++ b/tla/consensus/Traceccfraft.cfg @@ -51,7 +51,7 @@ CONSTANTS Candidate = Candidate Leader = Leader RetiredLeader = RetiredLeader - Pending = Pending + None = None RequestVoteRequest = RequestVoteRequest RequestVoteResponse = RequestVoteResponse diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla index 86d49c39e3de..ea1679e37639 100644 --- a/tla/consensus/Traceccfraft.tla +++ b/tla/consensus/Traceccfraft.tla @@ -8,7 +8,7 @@ RaftMsgType == "raft_propose_request_vote" :> ProposeVoteRequest LeadershipState == - Leader :> "Leader" @@ Follower :> "Follower" @@ Candidate :> "Candidate" @@ Pending :> "Pending" + Leader :> "Leader" @@ Follower :> "Follower" @@ Candidate :> "Candidate" @@ None :> "None" \* In: <<[idx |-> 0, nodes |-> [0 |-> [address |-> ":"]], rid |-> 0]>> \* Out: (0 :> {0}) @@ -380,16 +380,16 @@ TraceNext == RaftDriverQuirks == \* The "nodes" command in raft scenarios causes N consecutive "add_configuration" log lines to be emitted, - \* where N is determined by the "nodes" parameter. At this stage, the nodes are in the "Pending" state. + \* where N is determined by the "nodes" parameter. At this stage, the nodes are in the "None" state. \* However, the enablement condition of "ccfraft!Timeout" is only true for nodes in the "Candidate" or \* "Follower" state. Therefore, we include this action to address this quirk in the raft_driver. \/ /\ IsEvent("add_configuration") - /\ state[logline.msg.state.node_id] = Pending + /\ state[logline.msg.state.node_id] = None /\ configurations' = [ configurations EXCEPT ![logline.msg.state.node_id] = ToConfigurations(<>)] /\ state' = [ state EXCEPT ![logline.msg.state.node_id] = Follower ] /\ UNCHANGED <> \/ /\ IsEvent("become_follower") - /\ state[logline.msg.state.node_id] = Pending + /\ state[logline.msg.state.node_id] = None /\ configurations[logline.msg.state.node_id] = ToConfigurations(logline.msg.configurations) /\ state' = [ state EXCEPT ![logline.msg.state.node_id] = Follower ] /\ UNCHANGED <> diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla index f619448a4009..c45e55e6122c 100644 --- a/tla/consensus/ccfraft.tla +++ b/tla/consensus/ccfraft.tla @@ -48,21 +48,19 @@ CONSTANTS \* /\ state[s] = Leader \* /\ CurrentConfiguration(s) \ CurrentConfiguration(s)' = {s} \* => state'[s] = RetiredLeader]_state + \* TODO: this should be split into a separate membership_state, as in + \* the implementation. RetiredLeader, - \* The node has passed attestation checks, but is waiting for member confirmation, - \* and just isn't part of any configurations at all, nor has a communication channel - \* with other nodes in the network. - \* - \* More formally: - \* \A i \in Servers : state[i] = Pending => i \notin { GetServerSet(s) : s \in Servers} - Pending + \* Initial state for a joiner node, until it has received a first message + \* from another node. + None States == { Follower, Candidate, Leader, RetiredLeader, - Pending + None } \* Message types: @@ -497,7 +495,7 @@ InitMessagesVars == InitServerVars == /\ currentTerm = [i \in Servers |-> 0] - /\ state = [i \in Servers |-> IF i \in configurations[i][0] THEN Follower ELSE Pending] + /\ state = [i \in Servers |-> IF i \in configurations[i][0] THEN Follower ELSE None] /\ votedFor = [i \in Servers |-> Nil] InitCandidateVars == @@ -907,7 +905,7 @@ NoConflictAppendEntriesRequest(i, j, m) == /\ configurations' = [configurations EXCEPT ![i] = RestrictDomain(new_configs, LAMBDA c : c >= new_conf_index)] \* If we added a new configuration that we are in and were pending, we are now follower - /\ IF /\ state[i] = Pending + /\ IF /\ state[i] = None /\ \E conf_index \in DOMAIN(new_configs) : i \in new_configs[conf_index] THEN state' = [state EXCEPT ![i] = Follower ] ELSE UNCHANGED state @@ -923,7 +921,7 @@ NoConflictAppendEntriesRequest(i, j, m) == AcceptAppendEntriesRequest(i, j, logOk, m) == \* accept request /\ m.term = currentTerm[i] - /\ state[i] \in {Follower, Pending} + /\ state[i] \in {Follower, None} /\ logOk /\ LET index == m.prevLogIndex + 1 IN \/ AppendEntriesAlreadyDone(i, j, index, m) @@ -993,12 +991,12 @@ DropResponseWhenNotInState(i, j, m) == DropIgnoredMessage(i,j,m) == \* Drop messages if... /\ - \* .. recipient is still Pending.. - \/ /\ state[i] = Pending + \* .. recipient is still None.. + \/ /\ state[i] = None \* .. and the message is anything other than an append entries request /\ m.type /= AppendEntriesRequest - \* OR if message is to a server that has surpassed the Pending stage .. - \/ /\ state[i] /= Pending + \* OR if message is to a server that has surpassed the None stage .. + \/ /\ state[i] /= None \* .. and it comes from a server outside of the configuration /\ \lnot IsInServerSet(j, i) \* OR if recipient is RetiredLeader and this is not a request to vote @@ -1325,7 +1323,7 @@ MonotonicMatchIndexProp == PermittedLogChangesProp == [][\A i \in Servers : log[i] # log[i]' => - \/ state[i]' = Pending + \/ state[i]' = None \/ state[i]' = Follower \* Established leader adding new entries \/ /\ state[i] = Leader @@ -1347,7 +1345,7 @@ PermittedLogChangesProp == StateTransitionsProp == [][\A i \in Servers : - /\ state[i] = Pending => state[i]' \in {Pending, Follower} + /\ state[i] = None => state[i]' \in {None, Follower} /\ state[i] = Follower => state[i]' \in {Follower, Candidate} /\ state[i] = Candidate => state[i]' \in {Follower, Candidate, Leader} /\ state[i] = Leader => state[i]' \in {Follower, Leader, RetiredLeader} @@ -1355,8 +1353,8 @@ StateTransitionsProp == ]_vars PendingBecomesFollowerProp == - \* A pending node that becomes part of any configuration immediately transitions to Follower. - [][\A s \in { s \in Servers : state[s] = Pending } : + \* A pending node that becomes aware it is part of a configuration immediately transitions to Follower. + [][\A s \in { s \in Servers : state[s] = None } : s \in GetServerSet(s)' => state[s]' = Follower]_vars