From 3ed05339de02cbc80fcb1a2739c8f114588a40be Mon Sep 17 00:00:00 2001 From: achamayou Date: Wed, 22 Jul 2026 21:50:17 +0100 Subject: [PATCH 1/3] Add Raft scenario for former candidate double vote Reproduce the same-term second vote described in issue #5891 so trace validation captures the implementation/model divergence. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: 4735ff07-a8dd-48e9-8c20-01c6f665da7a --- .../former_candidate_double_vote | 87 +++++++++++++++++++ 1 file changed, 87 insertions(+) create mode 100644 tests/raft_scenarios/former_candidate_double_vote diff --git a/tests/raft_scenarios/former_candidate_double_vote b/tests/raft_scenarios/former_candidate_double_vote new file mode 100644 index 00000000000..ca3655a9edb --- /dev/null +++ b/tests/raft_scenarios/former_candidate_double_vote @@ -0,0 +1,87 @@ +# Reproduce https://github.com/microsoft/CCF/issues/5891. +# +# Node 1 first votes for itself in term 3. Node 2 wins the same term with votes +# from nodes 0 and 4, then sends node 1 an AppendEntries that node 1 cannot +# match. Node 1 steps down but does not learn the leader because it rejects the +# AppendEntries. A delayed vote request from node 3 then causes node 1 to vote +# a second time in term 3. +pre_vote_enabled,false + +start_node,0 +emit_signature,2 + +trust_nodes,2,1,2,3,4 +emit_signature,2 + +# Bring every node to the same committed prefix. +periodic_all,10 +dispatch_all +periodic_all,10 +dispatch_all +periodic_all,10 +dispatch_all +assert_state_sync +assert_commit_idx,0,4 + +# Give future leader node 2 a longer, uncommitted signature suffix. It retains +# this committable entry when elected, so its first heartbeat will refer to +# index 5, which node 1 does not have. +emit_signature,2 +periodic_one,0,10 +dispatch_single,0,2 +assert_last_txid,1,2.4 +assert_last_txid,2,2.5 + +# Remove the other replication messages and node 2's response so that the +# election message ordering below is explicit. +drop_pending,0 +drop_pending,2 + +# Nodes 1, 2, and 3 all become candidates in term 3 and vote for themselves. +periodic_one,1,100 +periodic_one,2,100 +periodic_one,3,100 +assert_detail,1,leadership_state,Candidate +assert_detail,2,leadership_state,Candidate +assert_detail,3,leadership_state,Candidate +assert_detail,1,current_view,3 +assert_detail,2,current_view,3 +assert_detail,3,current_view,3 + +# Retain only the vote requests needed for this reproduction. +drop_pending_to,1,0 +drop_pending_to,1,2 +drop_pending_to,1,4 +drop_pending_to,2,3 +drop_pending_to,3,0 +drop_pending_to,3,2 +drop_pending_to,3,4 + +# Nodes 0 and 4 elect node 2 as leader of term 3. +dispatch_single,2,0 +dispatch_single,0,2 +dispatch_single,2,4 +dispatch_single,4,2 +assert_detail,2,leadership_state,Leader +assert_detail,2,current_view,3 + +# Retain only node 2's request and unmatched AppendEntries to node 1. +drop_pending_to,2,0 +drop_pending_to,2,3 +drop_pending_to,2,4 + +# Node 1 first rejects node 2's queued vote request because it already voted +# for itself. It then receives node 2's unmatched AppendEntries and steps down. +dispatch_single,2,1 +assert_detail,1,leadership_state,Candidate +dispatch_single,2,1 +assert_detail,1,leadership_state,Follower +assert_detail,1,current_view,3 +assert_last_txid,1,2.4 + +# Node 1 now grants node 3's delayed vote request in the same term. Deliver the +# older request from node 1 first, followed by this second granted vote. +dispatch_single,3,1 +drop_pending_to,1,2 +dispatch_single,1,3 +dispatch_single,1,3 From 6a1d803aa8e36213eec1cce51cb81b4f28b21558 Mon Sep 17 00:00:00 2001 From: achamayou Date: Wed, 22 Jul 2026 22:19:30 +0100 Subject: [PATCH 2/3] Align Raft model with same-term vote reset Model CCF clearing votedFor when an AppendEntries message makes a candidate step down within its current term. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: 4735ff07-a8dd-48e9-8c20-01c6f665da7a --- tla/consensus/ccfraft.tla | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla index 134032dad5c..d7d88216981 100644 --- a/tla/consensus/ccfraft.tla +++ b/tla/consensus/ccfraft.tla @@ -1061,8 +1061,10 @@ ReturnToFollowerState(i, m) == /\ leadershipState[i] \in {PreVoteCandidate, Candidate} /\ leadershipState' = [leadershipState EXCEPT ![i] = Follower] /\ isNewFollower' = [isNewFollower EXCEPT ![i] = TRUE] + \* CCF clears its vote when stepping down, even within the same term + /\ votedFor' = [votedFor EXCEPT ![i] = Nil] \* Note that the set of messages is unchanged as m is discarded - /\ UNCHANGED <> \* Follower i receives a AppendEntries from leader j for log entries it already has From 6e95d565f80d5d7435e2930ff4065d4a9cd2e272 Mon Sep 17 00:00:00 2001 From: achamayou Date: Thu, 23 Jul 2026 07:23:25 +0100 Subject: [PATCH 3/3] Document same-term vote reset source Reference the Raft call site and voted_for reset lines from the matching TLA transition. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: 4735ff07-a8dd-48e9-8c20-01c6f665da7a --- tla/consensus/ccfraft.tla | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla index d7d88216981..e0e6f56e0b2 100644 --- a/tla/consensus/ccfraft.tla +++ b/tla/consensus/ccfraft.tla @@ -1061,7 +1061,8 @@ ReturnToFollowerState(i, m) == /\ leadershipState[i] \in {PreVoteCandidate, Candidate} /\ leadershipState' = [leadershipState EXCEPT ![i] = Follower] /\ isNewFollower' = [isNewFollower EXCEPT ![i] = TRUE] - \* CCF clears its vote when stepping down, even within the same term + \* Mirrors raft.h:1144: same-term AppendEntries calls + \* become_aware_of_new_term(), which clears voted_for at raft.h:2286. /\ votedFor' = [votedFor EXCEPT ![i] = Nil] \* Note that the set of messages is unchanged as m is discarded /\ UNCHANGED <