fix: remove side effects from pre-vote processing

[Qian-Cheng-nju]

Hi again — two small things I spotted in process_pre_vote while looking at the pre-vote path.

Right now process_pre_vote calls update_term (line 2942) and sets voted_for (line 2960) when granting a pre-vote. Per Raft thesis Section 9.6, pre-votes are meant to be side-effect-free on the receiver — the whole point is that a partitioned node can probe without disrupting the cluster.

The update_term call means a rejoining node's pre-vote inflates the cluster's terms, which is exactly what pre-vote is supposed to prevent. And setting voted_for means a pre-vote grant blocks a later real vote from a different candidate at the same term, which can delay elections.

This patch removes both side effects so pre-votes stay non-binding.

[kjnilsson]

it is right that the pre vote should not persist the voted for - if the term is higher though it should update that as it should always retain the highest term known.

[Qian-Cheng-nju]

Thanks @kjnilsson — you're right, restored update_term so the node always retains the highest known term. Now only the voted_for side effect is removed.

[kjnilsson]

Thanks @kjnilsson — you're right, restored update_term so the node always retains the highest known term. Now only the voted_for side effect is removed.

thank you, are you using your "Specula" tool to find these issues or are the manual finds?

[Qian-Cheng-nju]

These issues were all found using Specula! Specula is an automated verification tool that uses model checking to find bugs in distributed and concurrent system implementations that has already been adopted by teams at several companies, where it has uncovered real bugs. So far, Specula has found over 100 issues across a wide range of safety-critical systems in different domains, including HashiCorp Raft, GCC, CometBFT, and others (See case-studies). We're currently running Specula on various systems to continuously improve its effectiveness.

That said, I understand that community maintainers' time is valuable, so every issue reported here has been manually reviewed by me, and all PRs are hand-written and submitted by me personally. We genuinely want to contribute to the community rather than waste anyone's time. So far, the PRs we've submitted have been well-received by developers.

Thank you so much for reviewing these issues. We'd also sincerely welcome you to try Specula — it doesn't require any background in formal methods. In fact, developers who know their systems well are the ones who can find the most bugs with it. If you run into any issues while using it, feel free to reach out — we'd love to hear about any shortcomings so we can keep improving the tool. Thanks again for your thoroughness and dedication!