Repository navigation
rep: __rep_cmp_vote must be a total order (election can elect older data, data loss) - #266
Merged
Merged
Conversation
added 3 commits
November 4, 2026 10:57
Precondition reproduced against the real engine (dev box, non-diagnostic --enable-test --enable-tcl): two/three electable sites with EQUAL last-commit LSN (1/16402) and DIFFERENT data_gen (2 vs 3), real VOTE1 messages. Documents the arm-D mechanism and the open reachability question (stale site elected only if tallied last at a majority). Not yet a passing/failing gate; WIP probe.
…gen bypass)
The election winner comparator __rep_cmp_vote (src/rep/rep_elect.c) was not a
consistent order, with two defects:
1. The first vote (rep->sites == 1) was adopted outright, so the winner
depended on which vote a site tallied first.
2. The last arm (equal LSN => higher priority / tiebreaker) fired regardless
of data_gen, so a vote with an OLDER data_gen but an equal LSN and a
higher priority or tiebreaker could beat a vote with a NEWER data_gen.
Defect 2 is a durability bug, not just a failure to settle: electing a site
with older data rolls back a commit the newer site already had (a client
memcmp's the log bytes at its verify LSN in __rep_verify, so a wrong winner
genuinely truncates the loser's tail). The precondition -- two electable
sites with EQUAL last-commit LSN and DIFFERENT data_gen -- was reproduced
against the live engine (test/rep/E1-FINDINGS.md): a VOTE1 carries the LSN of
the last __txn_regop and the highest gen in REPLSNHIST, and these are
independent, so equal LSN with different data_gen is reachable.
Rewrite __rep_cmp_vote as a single TOTAL ORDER, applied uniformly to every
vote including the first: electable > not; non-zero priority > zero (the
mixed-version ELECTABLE semantics are preserved); then data_gen, LSN, priority,
tiebreaker, and finally eid as the always-distinct discriminator so the
relation is total even if two sites draw equal random tiebreakers. Because
rep->winner is not reset between elections, the first vote is detected by
rep->sites == 1 (reset in __rep_elect_done), not by rep->winner.
Gate: test/db/run_rep_cmpvote_order.sh drives a verbatim copy of the real
comparator (drift-checked by check_rep_cmpvote_copy.sh) over the captured vote
vectors in every arrival order; it PASSES on the fix and FAILS with -DCMPVOTE_OLD
(the pre-fix comparator). lts/2026.10.7 has the identical function; backport to
follow.
test/rep/E1-FINDINGS.md: the full write-up for the __rep_cmp_vote defect -- what is proven (comparator non-total-order; the equal-LSN/different-data_gen precondition reproduced against the live engine), what is argued (a real network delivering the stale VOTE1 last at a majority), the fix, and the mixed-version rolling-upgrade analysis with a user-facing upgrade note. test/tcl/rep200.tcl: an ADVISORY reproduction that builds the precondition (three electable sites, equal last-commit LSN, data_gen 2/3/3) against the real engine and reports it; its header explains why a deterministic end-to-end TCL election gate is not possible here and points to the comparator-level gate (test/db/run_rep_cmpvote_order.sh) and the CBMC harness as the pass/fail checks.
Contributor
Coccinelle convention checksNo new violations. ✅ Resolved since baseline (3) -- update dist/cocci/baseline.txt to lock these in. |
Contributor
ABI diff vs
|
This was referenced Nov 4, 2026
…s not do The comment called eid an always-distinct discriminator that makes every site agree on the winner. eids are local: repmgr numbers sites in the order it learns of them, so two sites can give the same peer different eids. The eid step makes each site's order total, which is what order independence needs. Agreement between sites rests on the random 32-bit tiebreaker, as it did before; an exact collision costs an extra election round, not a second master. Comment-only; the copy in rep_cmpvote_order.c follows.
Collaborator
Author
|
Lead review: the fix is right and the runner fails on the old code and passes on the new (re-run locally). One overclaim corrected in c6e1030: the comment said the eid step makes every site agree on the winner. eids are local (repmgr numbers sites in the order it learns of them), so two sites can give the same peer different eids. The eid step makes each site's order total, which is what order independence needs. Agreement between sites still rests on the random 32-bit tiebreaker, as before; an exact collision costs an extra election round, not a second master. Comment-only. The diagnostic-build rep panic E1 found is a checker bug, fixed separately in #268. |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
E1:
__rep_cmp_votemust be a total order (election can elect older data)The election winner comparator
__rep_cmp_vote(src/rep/rep_elect.c) was nota consistent order, with two defects (CBMC H1 finding on #263, "Counterexample
1" and "Counterexample 2"):
rep->sites == 1) wasadopted outright, so the winner depended on arrival order.
cmp == 0 && (priority/tiebreaker …))fired whenever the LSNs were equal regardless of data_gen, so a vote
with an OLDER data_gen but an equal LSN and a higher priority or tiebreaker
could beat a vote with a NEWER data_gen.
Defect 2 is a durability bug, not only liveness. Electing a site with older
data rolls back the newer site's tail on sync — a client
memcmps the logbytes at its verify LSN (
__rep_verify, rep_verify.c:77), so a wrong winnertruncates the loser's log and loses a commit that was already durable.
What is proven vs argued
old code); and the precondition is reachable on real sites — two/three
electable sites with EQUAL last-commit LSN and DIFFERENT data_gen, carrying
those values in real VOTE1 messages, reproduced against the live engine
(dev box). A VOTE1's LSN is the last
__txn_regopand its data_gen is thehighest REPLSNHIST gen; these are independent, so equal LSN + different
data_gen is reachable, and no invariant forbids it.
(an ordinary, non-zero-probability event) so the stale site is actually
elected. Full write-up and the mixed-version rolling-upgrade analysis +
user-facing upgrade note are in
test/rep/E1-FINDINGS.md.The fix
__rep_cmp_voteis rewritten as a single total order applied uniformly toevery vote including the first (keyed on
rep->sites == 1, sincerep->winneris not reset between elections): electable > not; non-zero priority > zero
(mixed-version ELECTABLE preserved); then data_gen, LSN, priority,
tiebreaker, and finally eid as the always-distinct discriminator so the
relation is total even if two sites draw equal random tiebreakers.
No format / ABI / region change.
Tests
test/db/run_rep_cmpvote_order.sh— the deterministic gate: drives averbatim copy of the real comparator (drift-checked by
check_rep_cmpvote_copy.sh) over the captured real vote vectors in everyarrival order. PASSES on the fix, FAILS with
-DCMPVOTE_OLD(the 2-sitestale-vs-newer case: arrival order flips the winner between the newer and the
stale site). In
test/MANIFEST(db tier), so it runs underrun_all.sh.test/tcl/rep200.tcl— ADVISORY: reproduces the precondition (threeelectable sites, equal LSN, data_gen 2/3/3) against the real engine every
run. Its header explains why a deterministic end-to-end TCL election gate is
not possible here (egen vs data_gen coupling in the harness) and points to
the comparator-level gate.
test/cbmc/harness_cmpvote.cupdate (see below) proves (a) orderindependence and (e) data_gen-maximality on the fix; the old code is the
sabotage arm and fails both.
Regressions (dev box, non-diagnostic
--enable-test --enable-tcl)rep001–rep020and the election set (rep002/005/016/020/022/026/063/067/069/ 076/093/094) all PASS on both master-baseline and the fix, identical — noregression.
Note: the
--enable-diagnosticrep election tests panic on a pre-existingRFC 0010 A3 lock-order artifact in
src/rep/rep_backup.c(the TCL testtransport re-enters
__memp_fgetunder rep latches); this reproducesidentically on plain master and is unrelated to this change (flagged to the
lead separately).
CBMC harness + LTS
The
test/cbmc/harness_cmpvote.c/run.sh/ README-H1 update lives on #263(the branch that adds
harness_cmpvote.c); it is prepared and verified butdepends on this fix being in the same tree (
check_copies.sh), so the leadsequences it when reconciling #263 with this fix.
lts/2026.10.7has theidentical function — backport PR:
backport/2026.10.7/rep-elect-datagen.