PreVote enabled in TLA model checking #7404
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Contributor
There was a problem hiding this comment.
Pull Request Overview
This PR implements PreVote support in the TLA+ model checking specification for CCF Raft consensus. PreVote is a mechanism where followers must first prove they could be elected (via a speculative vote round) before becoming actual candidates, helping prevent disruptive election attempts.
Key changes:
- Added
PreVoteCandidateleadership state betweenFollowerandCandidate - Introduced
preVoteEnabledconfiguration variable to allow testing both with and without PreVote - Modified election logic to require majority pre-votes before transitioning to full candidacy
Reviewed Changes
Copilot reviewed 7 out of 7 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| tla/consensus/ccfraft.tla | Core PreVote implementation: new state, configuration variable, updated transitions and message handlers |
| tla/consensus/Traceccfraft.tla | Updated trace validation to include configVars in UNCHANGED clauses |
| tla/consensus/Traceccfraft.cfg | Added PreVoteCandidate constant mapping |
| tla/consensus/SIMccfraft.tla | Added simulation init to non-deterministically set preVoteEnabled |
| tla/consensus/SIMccfraft.cfg | Configured simulation to use new init function |
| tla/consensus/MCccfraft.tla | Added model checking init and debug invariant for PreVote |
| tla/consensus/MCccfraft.cfg | Added PreVoteCandidate constant and debug invariant |
achamayou
reviewed
Oct 28, 2025
achamayou
reviewed
Oct 28, 2025
achamayou
reviewed
Oct 28, 2025
achamayou
reviewed
Oct 28, 2025
Contributor
Author
|
This should be ready for review. I've cancelled the CI for now. Will rebase on main when the CI is quieter. |
achamayou
approved these changes
Oct 29, 2025
cjen1-msft
added
2.x-todo
cjen1-msft
added a commit
to cjen1-msft/CCF
that referenced
this pull request
Nov 5, 2025
Co-authored-by: Amaury Chamayou <amchamay@microsoft.com>
cjen1-msft
added a commit
to cjen1-msft/CCF
that referenced
this pull request
Nov 5, 2025
Co-authored-by: Amaury Chamayou <amchamay@microsoft.com>
eddyashton
added
backported
Member
|
Adding backported label - this was backported in #7436. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Put succinctly, pre-vote requires that a follower must prove that it could be elected before becoming a candidate.
This is implemented as a special follower state:
PreVoteCandidatewhere the follower sends speculative requestVote messages.These RequestVotes do not have any actual change on the receiving node, but notify the PreVoteCandidate that that node would have voted for it.
This is a minimal PR to start getting model checking of this.
The current PR has: