From c48b553b4e1b0db9f9e97dad209b0a2b118de0f3 Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Tue, 9 Jan 2024 17:28:03 +0000 Subject: [PATCH] TV for startup followed by join (#5839) --- tests/raft_scenarios/startup_2nodes | 14 ++++++++++++++ tla/consensus/Traceccfraft.tla | 3 ++- tla/consensus/ccfraft.tla | 17 ++++++++++++----- 3 files changed, 28 insertions(+), 6 deletions(-) create mode 100644 tests/raft_scenarios/startup_2nodes diff --git a/tests/raft_scenarios/startup_2nodes b/tests/raft_scenarios/startup_2nodes new file mode 100644 index 000000000000..8e1fec5062c5 --- /dev/null +++ b/tests/raft_scenarios/startup_2nodes @@ -0,0 +1,14 @@ +start_node,0 +assert_is_primary,0 +emit_signature,2 + +assert_is_primary,0 +assert_commit_idx,0,2 + +trust_node,2,1 +emit_signature,2 + +dispatch_all +# periodic_all,10 +# dispatch_all +# assert_commit_idx,0,4 \ No newline at end of file diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla index 345d63e3420e..f4d6e6fc0f27 100644 --- a/tla/consensus/Traceccfraft.tla +++ b/tla/consensus/Traceccfraft.tla @@ -176,7 +176,8 @@ IsSendAppendEntries == /\ IsAppendEntriesRequest(msg, j, i, logline) \* There is now one more message of this type. /\ Network!OneMoreMessage(msg) - /\ logline.msg.sent_idx = sentIndex[i][j] +\* TODO revisit once nextIndex-related changes are merged in the spec +\* /\ logline.msg.sent_idx = nextIndex[i][j] /\ logline.msg.match_idx = matchIndex[i][j] /\ committableIndices[logline.msg.state.node_id] = Range(logline.msg.state.committable_indices) diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla index efd67bb3510d..7cc431cec042 100644 --- a/tla/consensus/ccfraft.tla +++ b/tla/consensus/ccfraft.tla @@ -645,6 +645,12 @@ ChangeConfigurationInt(i, newConfiguration) == \* i.e., be re-added to a new configuration. Instead, the node has to rejoin with a \* "fresh" identity (compare sec 6.2, page 8, https://arxiv.org/abs/2310.11559). /\ \A s \in newConfiguration: s \notin removedFromConfiguration + \* See raft.h:2401, nodes are only sent future entries initially, they will NACK if necessary. + \* This is because they are expected to start from a fairly recent snapshot, not from scratch. + /\ LET + addedNodes == newConfiguration \ CurrentConfiguration(i) + newSentIndex == [ k \in Servers |-> IF k \in addedNodes THEN Len(log[i]) ELSE sentIndex[i][k]] + IN sentIndex' = [sentIndex EXCEPT ![i] = newSentIndex] \* Keep track of running reconfigurations to limit state space /\ reconfigurationCount' = reconfigurationCount + 1 /\ removedFromConfiguration' = removedFromConfiguration \cup (CurrentConfiguration(i) \ newConfiguration) @@ -653,7 +659,7 @@ ChangeConfigurationInt(i, newConfiguration) == configuration |-> newConfiguration, contentType |-> TypeReconfiguration])] /\ configurations' = [configurations EXCEPT ![i] = configurations[i] @@ Len(log'[i]) :> newConfiguration] - /\ UNCHANGED <> + /\ UNCHANGED <> ChangeConfiguration(i) == \* Reconfigure to any *non-empty* subset of servers. ChangeConfigurationInt checks that the new @@ -940,7 +946,8 @@ HandleAppendEntriesResponse(i, j, m) == UpdateTerm(i, j, m) == /\ m.term > currentTerm[i] /\ currentTerm' = [currentTerm EXCEPT ![i] = m.term] - /\ state' = [state EXCEPT ![i] = IF @ \in {Leader, Candidate} THEN Follower ELSE @] + \* See become_aware_of_new_term() in raft.h:1915 + /\ state' = [state EXCEPT ![i] = IF @ \in {Leader, Candidate, None} THEN Follower ELSE @] /\ votedFor' = [votedFor EXCEPT ![i] = Nil] \* See rollback(last_committable_index()) in raft::become_follower /\ log' = [log EXCEPT ![i] = SubSeq(@, 1, LastCommittableIndex(i))] @@ -1224,13 +1231,14 @@ MonoLogInv == LogConfigurationConsistentInv == \A i \in Servers : \/ state[i] = None + \* Follower, but no known configurations yet + \/ /\ state[i] = Follower + /\ Cardinality(DOMAIN configurations[i]) = 0 \/ \* Configurations should have associated reconfiguration txs in the log /\ \A idx \in DOMAIN (configurations[i]) : /\ log[i][idx].contentType = TypeReconfiguration /\ log[i][idx].configuration = configurations[i][idx] - \* Current configuration should be committed - /\ commitIndex[i] >= CurrentConfigurationIndex(i) \* Pending configurations should not be committed yet /\ Cardinality(DOMAIN configurations[i]) > 1 => commitIndex[i] < NextConfigurationIndex(i) @@ -1252,7 +1260,6 @@ NoLeaderBeforeInitialTerm == \* we might wish to add it in the future. This could be achieved by updating \* nextIndex to max of current nextIndex and matchIndex when an AE ACK is received. MatchIndexLowerBoundSentIndexInv == - \A i,j \in Servers : state[i] = Leader => sentIndex[i][j] >= matchIndex[i][j]