From e6b234a6a4cfcebbd96653a81866d7b237ac6143 Mon Sep 17 00:00:00 2001 From: Rongsong Shen Date: Tue, 16 Jun 2026 07:18:06 +0000 Subject: [PATCH] test(ha-prevote): Raft safety-invariant property tests + RN-1 consistency argument (task 6.1) Four property-style raft tests proving the PreVote API preserves the safety invariants: term/voted_for/role never change and on_persist never fires across mixed begin/request/reply sequences (WON and LOST); a WON round creates no leader (stays FOLLOWER); and the real-vote higher-term-adopt + step-down + quorum-elect path is unchanged (bug-339/340 intact). Records the TLA+/checklist consistency argument (RN-1) in test_raft.c and research.md, citing the tests as evidence. Raft suite 123/0/0; zero production change. Co-Authored-By: Claude Opus 4.8 (1M context) --- .kiro/specs/ha-prevote/research.md | 253 ++++++++++++++++++++++++ .kiro/specs/ha-prevote/tasks.md | 2 +- src/lib/testsuite/test_raft.c | 303 +++++++++++++++++++++++++++++ 3 files changed, 557 insertions(+), 1 deletion(-) create mode 100644 .kiro/specs/ha-prevote/research.md diff --git a/.kiro/specs/ha-prevote/research.md b/.kiro/specs/ha-prevote/research.md new file mode 100644 index 0000000..36cd8a5 --- /dev/null +++ b/.kiro/specs/ha-prevote/research.md @@ -0,0 +1,253 @@ +# Gap Analysis: ha-prevote + +_Generated by `/kiro-validate-gap`. Informational — presents options and research items, not final design decisions._ + +## Analysis Summary + +- **The fix must be sender-side.** The disruptive step-down occurs in `raft_on_vote_request` Step 2 (raft.c:125-134) — term adoption + leader demotion — which runs **before** the `on_vote_eligible` gate (Step 5). No receiver gate today can save a healthy leader from a *fresh, higher-term* `RequestVote`, because the term is already adopted before any stickiness check. PreVote prevents the term inflation at the source. +- **Most receiver-side gating already exists.** `raft_cb_vote_eligible` (ha.c:217-245) already implements PRIMARY-deny, fresh-heartbeat-on-standby deny (leader stickiness), and catch-up deny; the dispatcher already enforces the freshness floor via `ha_vote_self_freshness`. PreVote evaluation can largely **reuse these gates** but must run with **zero state mutation**. +- **The new machinery is the candidate-side PreVote round** plus a wire message and a way to tally PreVote replies without touching `term`/`voted_for`. +- **Recommended shape: Hybrid (Option C).** New PreVote state in the raft library + new wire message/opcode, reusing the existing `ha_elect_ctx_t` collection, dispatcher freshness gate, and `raft_cb_vote_eligible` semantics. +- **Effort: M (3–7 days). Risk: Medium** — touches the safety-critical election path and the TLA+-referenced invariants, but integrates with well-factored, test-covered seams. + +--- + +## 1. Current State Investigation + +### Election path (raft library — `src/lib/raft/raft.c`, `raft.h`) + +- **State** (`raft_state_t`, raft.h:23-38): `term`, `role` (`RAFT_FOLLOWER|CANDIDATE|LEADER`), `voted_for`, `voted_for_term`, `votes_granted`, `replies_received`, `election_decided`, `election_timeout_ms`, `my_priority`. **No pre-vote fields.** +- **Callbacks** (`raft_callbacks_t`, raft.h:66-96): `on_send_vote_request(ctx, peer_idx, term)`, `on_vote_eligible(ctx, from_idx, term)`, `on_become_leader`, `on_become_follower`, `on_persist(ctx, term, voted_for)`, `on_schedule_timeout`, `on_cancel_timeout`, `on_start_election_after_delay`, `on_trace`. +- **`raft_start_election`** (raft.c:61-108): increments `term`, sets self-vote, **persists**, then sends `on_send_vote_request` to each peer, schedules timeout. Single-node short-circuit promotes immediately. +- **`raft_on_vote_request`** (raft.c:110-191): 6-step flow — (1) stale-term deny; (2) **term upgrade → adopt term, clear vote, step down, fire `on_become_follower` if was LEADER** (the disruptive path); (3) LEADER role deny; (4) one-vote-per-term; (5) `on_vote_eligible` policy gate; (6) persist-then-grant. +- **`raft_on_vote_reply`** (raft.c:193-252): term-upgrade demotion; quorum = `(n_peers/2)+1`; all-replied-no-quorum fallback. +- **Triggers**: `raft_on_leader_lost` → `on_start_election_after_delay` (priority jitter); `raft_check_and_start_election` (raft.c:282-294) skips if already voted for another, else `raft_start_election`. + +### Controller adapter (`src/controller/cluster.c`, `ha.c`, `ha.h`) + +- **Dispatch** (`cluster.c` `OPCode_requestVote`, lines 359-408): parses `request_vote_req_t`, computes freshness floor via `ha_vote_self_freshness` (max of local and learned-committed tag/LSN), applies `freshness_ok`, maps candidate name → index, then calls `raft_on_vote_request`. +- **Candidate send** (`ha.c` `on_vote_connected`, lines 2579-2610): builds `request_vote_req_t` (term, candidate_id, config_tag, last_log_lsn), sends via `xce_request` (or `xce_vote_request_hook` under `XCE_TESTING`). +- **Collection** (`ha_elect_ctx_t`, ha.h:75-116): flexible-array `votes[]`, `votes_granted` (init 1 = self), `n_replied`, `max_resp_tag/lsn` (yield gate), `done` semaphore. `handle_request_vote_reply` (ha.c:2473-2528) tallies and calls `ha_elect_evaluate_and_signal`. Quorum = `(n_peers+1+1)/2`. +- **Voter gate** (`raft_cb_vote_eligible`, ha.c:217-245): PRIMARY → deny; STANDBY + `ha_heartbeat_is_fresh` → deny; in catch-up → deny; else eligible (freshness already enforced by dispatcher). +- **Leader stickiness primitive** (`ha_heartbeat_is_fresh`, ha.c:2013-2022): `(now - last_activity) < heartbeat_timeout_ms`. `ha_on_heartbeat_received` updates `last_activity`. +- **Election initiation** (`ha_start_election_async`, ha.c:3341-3410): allocates `ha_elect_ctx_t`, sets self-vote, stores `ha->elect_ctx`, delegates to `raft_start_election`. +- **Election triggers**: `ha_on_primary_ctrl_fd_rdhup` (ha.c:3486) on connection loss; `liveness_poll_fn` (ha.c:3684-3722) on heartbeat timeout. + +### Wire schema (`src/schema/controller.capnp`) + +```capnp +struct RequestVoteRequest { # lines 796-801 + term @0; candidateId @1; configTag @2; lastLogLsn @3; +} +struct RequestVoteReply { # lines 803-808 + term @0; voteGranted @1; peerConfigTag @2; peerLastLogLsn @3; +} +``` +`OPCode` is an enum (lines 10-49); `requestVote @32` (line 43). **No PreVote opcode.** + +### Test seams + +- `xce_vote_request_hook` (ha.c:2560) intercepts the candidate send without live iomgr/SSL. +- `src/lib/testsuite/test_raft.c` — raft library unit tests with mock callbacks (TLA+ invariants). +- `src/controller/testsuite/`: `test_ha_election.c`, `test_ha_vote_gate.c`, `test_ha_start_election_async.c`, `test_ha_vote_send.c`, `test_ha_liveness.c`, `test_ha_role_lifecycle.c`, `test_ha_failover.c`. + +### Relevant constants (`ha.h:121-129`) + +`HEARTBEAT_INTERVAL_MS=3000`, `HEARTBEAT_TIMEOUT_MS=10000`, `ELECTION_TIMEOUT_MS=5000`, `ELECTION_JITTER_MAX_MS=200`, `ELECTION_PRIORITY_STEP_MS=500`. + +--- + +## 2. Requirement-to-Asset Map + +| Req | Capability needed | Existing asset | Gap | +|-----|-------------------|----------------|-----| +| **1** PreVote precedes term increment | A pre-election round that runs before `raft_start_election`; no persist/term change | `raft_start_election` (raft.c:61), `ha_start_election_async` (ha.c:3341) as the call site to gate | **Missing**: PreVote state + entry point; must interpose between trigger and `raft_start_election` | +| **1.2/1.3** No persistent mutation during PreVote | — | `on_persist` is only called by `raft_start_election`/`raft_on_vote_request` | **Constraint**: PreVote path must never call `on_persist` or mutate `term`/`voted_for` | +| **2** Voter eligibility reuses real-vote gate | Freshness + log-completeness check | Dispatcher freshness (`ha_vote_self_freshness`, cluster.c:389) + `raft_cb_vote_eligible` (ha.c:217) | **Constraint/Reuse**: run the same gate; must NOT record a vote | +| **2.3/2.4** No vote recorded; can still grant real vote later | — | one-vote-per-term lives in `raft_on_vote_request` Step 4 | **Constraint**: PreVote evaluation must bypass Steps 2/4/6 side effects | +| **3** Leader stickiness | Deny PreVote while leader believed alive; PRIMARY denies | `ha_heartbeat_is_fresh` (ha.c:2013), PRIMARY-deny in `raft_cb_vote_eligible` | **Reuse**: already present; just invoke from the PreVote receiver path | +| **3.1** Stickiness window semantics | "would not itself start an election" | Today: `heartbeat_timeout_ms` (10s) for freshness vs. `election_timeout_ms` (5s) probe | **Unknown (Research)**: which window defines stickiness — see RN-2 | +| **4** Frozen-then-resumed is non-disruptive | Candidate gets no PreVote majority → no term bump → re-attach | `ha_on_heartbeat_received` re-attach path | **Missing**: end-to-end behavior emerges from Req 1+3; needs integration test | +| **5** Legitimate changes still proceed | True death / partition heal still elect | `raft_on_vote_reply` term-upgrade demotion; existing failover (bug-339), rejoin (bug-340) | **Constraint**: do not regress; real-vote path unchanged after PreVote success | +| **6** Safety invariants | Election Safety, term monotonicity, Leader Completeness | `raft/raft.tla`, `test_raft.c`, controller verification checklist | **Constraint**: PreVote must be modeled/argued against TLA+; add invariant tests | +| **7.1** Transport compatibility | PreVote over existing election transport | capnp `OPCode`, `xce_request`, `peer_ctrl_msg_handler` | **Missing**: new opcode/flag + reply + dispatch case | +| **7.2/7.3** Observability | Log PreVote denials / abandoned campaigns | `on_trace` callback, `tlog` | **Missing**: trace/log points on PreVote deny + campaign abandonment | + +Gap tags: **Missing** = no asset; **Constraint** = existing behavior bounds the design; **Reuse** = asset directly applicable; **Unknown** = research item. + +--- + +## 3. Implementation Approach Options + +### Option A — Extend the existing RequestVote path with an `isPreVote` flag +Add `isPreVote @4 :Bool = false` to `RequestVoteRequest` (and a matching flag/struct for the reply). Reuse the same dispatch case, same `on_vote_connected` send, and branch inside `raft_on_vote_request` / `raft_cb_vote_eligible` on the flag to skip all state mutation. + +- ✅ Smallest wire change; backward-compatible capnp default; one RPC path. +- ✅ Reuses send/collect/gate machinery almost verbatim. +- ❌ Risks branching the safety-critical `raft_on_vote_request` with "if pre_vote skip steps 2/4/6" — easy to get a side-effect leak wrong. +- ❌ Overloads one function with two semantics (real vs. hypothetical). + +### Option B — New PreVote opcode + dedicated PreVote functions +Add `preVoteRequest`/`preVoteReply` opcodes and `PreVoteRequest`/`PreVoteReply` structs; add `raft_start_pre_vote`, `raft_on_pre_vote_request`, `raft_on_pre_vote_reply`, and `raft_cb_pre_vote_eligible`; a parallel (or shared) `ha_elect_ctx_t` pre-vote tally. + +- ✅ Clean separation; the pure (no-side-effect) PreVote functions are trivially auditable against the safety invariants. +- ✅ Real-vote path stays byte-for-byte unchanged (zero regression risk to bug-339/340). +- ❌ More new files/symbols and a second dispatch/collection path. +- ❌ Some duplication of freshness/eligibility logic unless carefully shared. + +### Option C — Hybrid (recommended) +New PreVote **wire message + raft state-machine functions** (Option B's clarity for the safety-critical core), but **reuse** the controller-side assets: the dispatcher freshness computation, `raft_cb_vote_eligible` semantics (called read-only), the `ha_elect_ctx_t` collection (add a `pre_votes_granted` counter or a `phase` field rather than a whole second struct), and `xce_vote_request_hook` for tests. + +- ✅ Keeps the pure PreVote decision isolated and auditable while avoiding duplicate collection/gate code. +- ✅ Real-vote path untouched; PreVote success simply calls the existing `raft_start_election`. +- ✅ Maps onto existing test seams (extend `test_ha_vote_gate.c`, add PreVote cases to `test_raft.c`). +- ❌ Requires a deliberate decision on shared-vs-separate eligibility helper to avoid drift. + +--- + +## 4. Effort & Risk + +| Dimension | Rating | Justification | +|-----------|--------|---------------| +| **Effort** | **M (3–7 days)** | New wire message + raft PreVote functions + candidate round + tests; but heavy reuse of existing gates, collection, and transport. | +| **Risk** | **Medium** | Touches the election safety core and TLA+-referenced invariants; mitigated by well-factored callback seams, existing gate logic to reuse, and strong test coverage. Highest-risk subtlety: ensuring the PreVote path has **zero** persistent side effects. | + +--- + +## 5. Recommendations for Design Phase + +**Preferred approach:** Option C (Hybrid). + +**Key decisions to finalize in design:** +1. **Wire representation** — separate `preVoteRequest`/`preVoteReply` opcodes (recommended for auditability) vs. `isPreVote` flag on the existing struct. Either is capnp-compatible; the opcode keeps the real-vote path provably untouched. +2. **Eligibility sharing** — factor the freshness + `raft_cb_vote_eligible` checks into a read-only helper callable from both the real-vote and PreVote receiver paths, so the two cannot drift. +3. **Collection reuse** — extend `ha_elect_ctx_t` with a PreVote phase/counter rather than a second struct. +4. **PreVote success → real election** — on PreVote majority, call the **unchanged** `raft_start_election`; confirm the candidate re-checks leader-stickiness was still absent at the moment of starting the real round. +5. **Defense-in-depth question** — decide whether to *also* add leader-stickiness gating to the real `raft_on_vote_request` term-upgrade path (Raft "reject RequestVote within min election timeout"), since PreVote alone leaves Step 2 able to step down a leader if a stray higher-term real RequestVote ever arrives. + +**Research Needed (carry to design):** +- **RN-1**: Model/argue the PreVote phase against `raft/raft.tla` and the controller verification checklist; confirm Election Safety + term monotonicity hold with the new path. (Req 6) +- **RN-2**: ✅ **RESOLVED — reuse `heartbeat_timeout_ms` via `ha_heartbeat_is_fresh()`.** See "Resolved Decisions → RN-2" below for the full comparison. (Req 3.1) +- **RN-3**: Confirm whether the PRIMARY should deny PreVotes via the existing `raft_cb_vote_eligible` PRIMARY-deny (Req 3.3) and that this composes with CheckQuorum-style behavior already present. +- **RN-4**: Decide PreVote round timeout/abandonment behavior and its interaction with the existing election jitter/priority and `election_timeout_ms` bounds (Req 5.4) — ensure no added unbounded delay. + +**Explicitly out of scope:** Backward/rolling-upgrade compatibility with peers that predate PreVote. The product is **pre-release**, so all controllers in a cluster deploy from the same build — there is no mixed-version (old-binary ↔ new-binary) cluster to support. The wire change (new opcode or struct field) may be made without a negotiation/fallback path. Req 7.1's "without disrupting real RequestVote/RequestVoteReply exchanges" refers to PreVote coexisting with the *concurrent same-version* real-vote path, not to inter-version compatibility. + +--- + +## 6. Resolved Decisions + +### RN-2 — Leader-stickiness window → reuse `heartbeat_timeout_ms` (Opt 1) + +**Decision:** The voter's leader-stickiness predicate is the existing `ha_heartbeat_is_fresh()` (`now − last_activity < heartbeat_timeout_ms`, currently 10s), gated on `role == CTRL_STANDBY`. PreVote introduces **no new timing concept**. + +**The governing invariant.** Stickiness is a single voter-side predicate: *"do I still believe a leader is alive?"* It must be **pinned to the failure-detection window** — the period during which the voter would not itself start an election. If the two diverge: +- **stickiness < failure-detection** → a gap opens where the voter grants a PreVote while still believing its leader is alive and not yet failing over → **reopens the disruption hole**. +- **stickiness > failure-detection** → a voter that has already decided the leader is dead (and is campaigning) still denies others' PreVotes → mutual denial → **PreVote majorities can't form → liveness stall**. + +So the window must equal whichever constant is XCE's *failure detector*. + +**Naming trap.** Textbook Raft overloads one "election timeout" for two roles; XCE separates them, so the dissertation's "reject votes within the minimum election timeout" maps to `HEARTBEAT_TIMEOUT_MS`, **not** `ELECTION_TIMEOUT_MS`: + +| Raft concept | XCE constant | Value | Role in XCE | +|---|---|---|---| +| election timeout *as leader-failure detector* | `HEARTBEAT_TIMEOUT_MS` | 10000 | Follower decides primary is dead → triggers failover (`liveness_poll_fn` / RDHUP) | +| election timeout *as vote-collection deadline* | `ELECTION_TIMEOUT_MS` | 5000 | Candidate waits this long for vote replies before giving up | +| heartbeat interval | `HEARTBEAT_INTERVAL_MS` | 3000 | Primary re-sends heartbeat every 3s | + +**Option comparison.** + +| | Opt 1: `heartbeat_timeout_ms` (10s) | Opt 2: `election_timeout_ms` (5s) | Opt 3: new `prevote_stickiness_ms` | Opt 4: `heartbeat_interval_ms` (3s) | +|---|---|---|---|---| +| Matches XCE failure-detector | ✅ exactly | ❌ wrong constant (vote-collection deadline) | ⚠️ only if set == 10s | ❌ far shorter | +| Consistent w/ existing real-vote gate (`raft_cb_vote_eligible`) | ✅ same predicate reused | ❌ real-vote 10s vs PreVote 5s drift | ⚠️ drift unless tuned | ❌ drift | +| Disruption gap (grant while leader alive) | ✅ none | ❌ [5s,10s] gap on flaky/asymmetric link | ⚠️ gap if < 10s | ❌ [3s,10s] gap | +| Tolerance to transient heartbeat loss | ✅ ~3 missed heartbeats | ⚠️ ~1 missed heartbeat | ⚠️ depends | ❌ 0 missed | +| Liveness-stall risk | ✅ none | ✅ none | ⚠️ stall if > 10s | ✅ none | +| Speeds up legitimate failover | n/a (matches today) | ❌ no real benefit¹ | ⚠️ only by also lowering failover timeout | ❌ no | +| New config surface | none | none | +1 tunable | none | + +¹ Under symmetric silent death nobody campaigns until the 10s failure-detection fires, so a shorter stickiness window has no candidate to grant to in [5s,10s] — zero speedup. A real crash closes sockets → RDHUP → standbys leave `CTRL_STANDBY` and campaign immediately, independent of the window. The shorter window's only observable effect is the disruption gap on a flaky link (a healthy primary missing ~2 of 3 heartbeats to one voter would get a PreVote granted against it at ~6s). + +**Why Opt 1.** It is the single value where the stickiness window, the failure-detection trigger (`liveness_poll_fn`), and the existing real-vote stickiness gate (`raft_cb_vote_eligible`) all key off **one predicate** (`ha_heartbeat_is_fresh`). Gating on `role == CTRL_STANDBY` also handles connection loss for free: RDHUP moves the node out of `CTRL_STANDBY`, so a genuinely disconnected voter stops being sticky immediately instead of waiting the full 10s. This is exactly what Req 3.1's observable phrasing ("received leader traffic recently enough that it would not itself start an election") already describes. If failover latency is later reduced by lowering `HEARTBEAT_TIMEOUT_MS`, stickiness follows automatically — which is itself the argument against Opt 3's separable constant. + +**Requirement impact:** Req 3.1 can be tightened in design (Boundary Commitment) to name `ha_heartbeat_is_fresh` / `heartbeat_timeout_ms` as the binding, while keeping the requirement text observable. + +--- + +## 7. Design Synthesis Outcomes (design phase) + +Applied the generalization / build-vs-adopt / simplification lenses before writing `design.md`. + +### Generalization — share interfaces, not implementations +PreVote and real-vote are two variations of "solicit a vote decision." Two seams are shared rather than duplicated: +- **Voter eligibility** — `raft_cb_vote_eligible` already encodes exactly the PreVote gates (PRIMARY-deny + fresh-heartbeat stickiness + catch-up-deny). The PreVote receiver reuses it verbatim via the existing `on_vote_eligible` callback; the only PreVote-specific rule is "decide without adopting the term." +- **Candidate tally** — `ha_elect_ctx_t` is reused with a `phase` discriminator (`HA_ELECT_PREVOTE` / `HA_ELECT_REAL`) instead of a second collection struct. Same quorum formula `(n_peers + 2) / 2`, same `votes[]` idempotency. + +The raft state-machine *functions* stay distinct (`raft_on_pre_vote_*` vs `raft_on_vote_*`) so the pure, no-side-effect PreVote path is independently auditable against the TLA+ model. + +### Build vs. Adopt — adopt +- **Algorithm**: Raft dissertation §9.6 PreVote (standard, well-specified). Not invented. +- **Infrastructure**: capnp election transport, iomgr/delaymgr, `ha_elect_ctx_t`, `ha_heartbeat_is_fresh`, `ha_vote_self_freshness`, `xce_vote_request_hook`. No new libraries. + +### Simplification decisions +- **Wire**: new `preVoteRequest`/`preVoteReply` **opcodes that reuse the existing `RequestVoteRequest`/`RequestVoteReply` structs and union arms** — no new capnp structs, and the real-vote handler stays byte-for-byte unchanged (zero regression risk to bug-339/340). Chosen over an `isPreVote` flag on the existing struct (which would branch the safety-critical real-vote handler). +- **Defer defense-in-depth** (the RN-4-adjacent / open "real-vote stickiness guard"): PreVote guarantees a candidate only sends a real RequestVote *after* a majority's stickiness has lapsed, so in a same-version cluster no stickiness-violating real RequestVote can arise. Adding the guard would touch the real-vote term-adoption path for no in-scope benefit. **Deferred**, documented in `design.md` → Architecture → Deferred decisions. (Resolves the open defense-in-depth question; RN-4 reduces to "bound the PreVote round with `election_timeout_ms` and re-arm liveness on loss," which the design specifies.) +- **No new role state**: the candidate stays `CTRL_STANDBY` during the PreVote round (tracked by `ctx.phase`), so a lost PreVote needs no rollback. The destructive `truncate-WAL + CTRL_ELECTING` step is **moved** from the failover trigger to PreVote success — the key change that makes a transient freeze a true no-op (Req 4). + +### Remaining open research item +- **RN-1**: TLA+ / verification-checklist argument that Election Safety + term monotonicity hold with the PreVote path (the real-vote path is unchanged, so this is largely an argument that the pure PreVote functions mutate nothing). Carried into implementation as `test_raft.c` invariant assertions. RN-3 (PRIMARY-deny composition) is resolved by reusing `raft_cb_vote_eligible`. + +--- + +## RN-1 resolved (task 6.1) + +**Decision/outcome:** The PreVote phase is consistent with the repository's +`raft/raft.tla` reference and the controller verification checklist — +Election Safety (≤1 leader per term), Leader Completeness, term monotonicity, +and a monotonic commit index all continue to hold with PreVote enabled. + +**Argument (purity ⇒ no new transitions).** + +1. **The PreVote functions are pure w.r.t. persistent Raft state.** Across an + arbitrary sequence of `raft_begin_pre_vote` / `raft_on_pre_vote_request` / + `raft_on_pre_vote_reply` calls — mixed grant+deny, duplicate replies, + out-of-range peers, and both WON and LOST terminal outcomes — none of them + ever writes `s->term`, `s->voted_for`, `s->voted_for_term`, or `s->role`, + and none invokes `on_persist`. Mechanical evidence: + `test_invariant_prevote_sequence_pure_no_persist` and + `test_invariant_prevote_lost_sequence_pure_no_persist` in + `src/lib/testsuite/test_raft.c`. + +2. **Term monotonicity is preserved.** Because the PreVote path writes no term, + the only writers of `s->term` remain the UNCHANGED `raft_start_election` + (the real, gated term bump) and `raft_on_vote_request` Step 2 (adopt a + strictly higher term). PreVote can only *gate* whether a real election + later runs; it never advances a term itself, and it never decreases one. + +3. **Election Safety is preserved.** Because the PreVote path creates no leader + (no `on_become_leader`, no `role := RAFT_LEADER`), it adds no new way to + satisfy the antecedent of Election Safety. A PreVote round reaching + `RAFT_PRE_VOTE_WON` returns a *status* only; the node stays `RAFT_FOLLOWER` + until the separate, unchanged `raft_start_election` / `raft_on_vote_reply` + path runs. Evidence: `test_invariant_prevote_won_grants_no_leadership`. + +4. **The bug-339/bug-340 failover path is unchanged.** The legitimate + higher-term-adopt + leader-step-down behavior lives entirely in + `raft_on_vote_request` / `raft_on_vote_reply`, which this feature does not + touch. PreVote sits strictly before that path and (by 1) leaves its inputs + untouched. Evidence: `test_invariant_real_vote_higher_term_adopt_unchanged` + demonstrates the real-vote path still adopts a higher term, fires + `on_become_follower` to step a leader down, and elects at quorum via + `on_become_leader` — even after a full PreVote round has run on the node. + +**Conclusion.** PreVote introduces no transition that writes a term or creates +a leader; every term-writing / leadership-creating transition in the model is +byte-for-byte the pre-PreVote transition. The set of reachable +`(term, leader)` configurations is therefore unchanged, so the `raft/raft.tla` +invariants (Election Safety, Leader Completeness, term monotonicity, monotonic +commit index) and the controller verification checklist continue to hold. The +four `test_invariant_*` tests are the mechanical evidence for premises (1)–(4), +and the existing failover/rejoin regression suites remain green with PreVote +enabled (controller suite 563 pass / 0 fail after task 4.2). Requirements +covered: 5.2, 5.3, 6.1, 6.2, 6.3, 6.4. diff --git a/.kiro/specs/ha-prevote/tasks.md b/.kiro/specs/ha-prevote/tasks.md index 40f0528..35b98b4 100644 --- a/.kiro/specs/ha-prevote/tasks.md +++ b/.kiro/specs/ha-prevote/tasks.md @@ -85,7 +85,7 @@ - _Depends: 4.1, 4.2, 5.1_ - [ ] 6. Validation: safety invariants and regression guard -- [ ] 6.1 Assert Raft safety invariants hold with PreVote +- [x] 6.1 Assert Raft safety invariants hold with PreVote - Add raft-library invariant assertions that the PreVote functions mutate no persistent state (Election Safety and term monotonicity preserved), and record the TLA+/verification-checklist consistency argument (the real-vote path is unchanged, so the higher-term-adopt failover and the bug-339/bug-340 fixes are preserved). - Observable: invariant tests pass and the existing failover/rejoin regression tests remain green with PreVote enabled. - _Requirements: 5.2, 5.3, 6.1, 6.2, 6.3, 6.4_ diff --git a/src/lib/testsuite/test_raft.c b/src/lib/testsuite/test_raft.c index 8aa688f..1c7b14e 100644 --- a/src/lib/testsuite/test_raft.c +++ b/src/lib/testsuite/test_raft.c @@ -3554,6 +3554,303 @@ static void test_pre_vote_reply_5node_won_at_three(void) TEST_ASSERT_EQUAL_INT(0, g_mock.become_follower_count); } +/* ====================================================================== * + * Task 6.1 — Raft safety-invariant assertions for the PreVote API + * + * The per-function tests above (tasks 2.1/2.2/2.3) check individual cases. + * The tests below assert the SAFETY INVARIANTS as *properties* that hold + * across the ENTIRE PreVote API, mechanically backing the RN-1 TLA+/ + * verification-checklist consistency argument recorded in + * .kiro/specs/ha-prevote/research.md (§"RN-1 resolved"). + * + * ---------------------------------------------------------------------- * + * RN-1 CONSISTENCY ARGUMENT (mechanically evidenced below) + * ---------------------------------------------------------------------- * + * Claim: adding the PreVote phase preserves every Raft safety invariant + * the repository's `raft/raft.tla` reference and the controller + * verification checklist require — Election Safety (at most one leader per + * term), Leader Completeness, term monotonicity, and a monotonic commit + * index — so the system stays consistent after the change. + * + * Proof structure (purity ⇒ no new transitions): + * + * 1. The three PreVote functions — raft_begin_pre_vote, + * raft_on_pre_vote_request, raft_on_pre_vote_reply — are PURE with + * respect to the persistent Raft state. Across an arbitrary sequence of + * begin / request / reply calls (mixed grant+deny, duplicates, + * out-of-range peers, and both WON and LOST terminal outcomes), none of + * them ever: + * - changes s->term, s->voted_for, s->voted_for_term, or s->role, or + * - invokes on_persist, or + * - invokes on_become_leader / on_become_follower. + * (Asserted by test_invariant_prevote_sequence_pure_no_persist and + * test_invariant_prevote_won_grants_no_leadership.) + * + * 2. Because the PreVote path mutates no term, it cannot violate term + * monotonicity: the only writer of s->term remains raft_start_election + * (real term bump) and raft_on_vote_request Step 2 (adopt a strictly + * higher term) — both UNCHANGED by this feature. A PreVote can only + * *gate* whether raft_start_election is later called; it never advances + * a term itself. (Asserted by the term-constant checks below.) + * + * 3. Because the PreVote path creates no leader (no on_become_leader, no + * role := RAFT_LEADER), it adds no new way to satisfy the antecedent of + * Election Safety. The sole leadership-creating transitions remain + * raft_start_election's single-node short-circuit and + * raft_on_vote_reply's quorum branch — again UNCHANGED. A PreVote round + * reaching RAFT_PRE_VOTE_WON returns a STATUS only; the node stays + * RAFT_FOLLOWER until the separate, unchanged real-election path runs. + * (Asserted by test_invariant_prevote_won_grants_no_leadership.) + * + * 4. The legitimate higher-term-adopt failover path (the bug-339/bug-340 + * fix) lives entirely in raft_on_vote_request / raft_on_vote_reply, + * which this feature does not touch. PreVote sits strictly *before* that + * path and, by (1), leaves its inputs (term/voted_for/role) untouched. + * test_invariant_real_vote_higher_term_adopt_unchanged demonstrates the + * real-vote path still adopts a higher term and fires become_follower / + * become_leader exactly as before, even after a full PreVote round has + * run on the same node — so PreVote did not alter the legitimate + * failover semantics bug-339/bug-340 depend on. + * + * Conclusion: PreVote introduces no transition that writes a term or + * creates a leader. Every term-writing / leadership-creating transition in + * the model is byte-for-byte the pre-PreVote transition. Therefore the set + * of reachable (term, leader) configurations is unchanged, and the TLA+ + * invariants (Election Safety, Leader Completeness, term monotonicity, + * monotonic commit index) and the controller verification checklist + * continue to hold. The tests below are the mechanical evidence for + * premises (1)–(4). + * ====================================================================== */ + +/* + * test_invariant_prevote_sequence_pure_no_persist (Req 6.2, 2.3, 1.2) + * + * PROPERTY (term monotonicity / no persistent mutation): drive a long, + * mixed sequence of PreVote operations through a node and assert that across + * the WHOLE sequence the persistent Raft state (term, voted_for, + * voted_for_term, role) never changes and on_persist is NEVER called. + * + * The sequence deliberately exercises: begin → answer an incoming request + * (grant) → answer a stale-term request (deny) → reply tally with a grant, + * a duplicate of that grant, an out-of-range peer, and a deny — i.e. every + * PreVote entry point and both grant/deny outcomes, including a WON + * terminal. If ANY PreVote code path leaked a term/vote/role write or a + * persist, this property fails — which would be a real Election-Safety / + * term-monotonicity finding, not a test bug. + */ +static void test_invariant_prevote_sequence_pure_no_persist(void) +{ + raft_state_t s; + raft_callbacks_t cbs = make_mock_cbs(); + + cbs.on_vote_eligible = mock_vote_eligible; + cbs.on_trace = mock_trace; + reset_mock(); + g_mock.vote_eligible_return_value = 1; /* grant when consulted */ + + /* 3-node FOLLOWER at term=5, having voted for peer 1 in an earlier term. + * These persistent values are the canary: nothing below may change them. */ + TEST_ASSERT_EQUAL_INT(0, init_vote_node(&s, &cbs, 3, 0, 5)); + s.voted_for = 1; + s.voted_for_term = 4; + + const uint64_t term0 = s.term; + const int voted_for0 = s.voted_for; + const uint64_t voted_for_term0 = s.voted_for_term; + const raft_role_t role0 = s.role; + + /* (a) begin a round — self-grant + prospective term, no persist */ + TEST_ASSERT_EQUAL_INT(0, raft_begin_pre_vote(&s)); + + /* (b) answer an incoming PreVote request that PASSES eligibility — grant */ + TEST_ASSERT_EQUAL_INT(1, raft_on_pre_vote_request(&s, 2, 6 /* higher */)); + + /* (c) answer a STALE-term incoming request — deny */ + TEST_ASSERT_EQUAL_INT(0, raft_on_pre_vote_request(&s, 2, 3 /* stale */)); + + /* (d) answer an incoming request the eligibility gate REJECTS — deny */ + g_mock.vote_eligible_return_value = 0; + TEST_ASSERT_EQUAL_INT(0, raft_on_pre_vote_request(&s, 2, 6)); + g_mock.vote_eligible_return_value = 1; + + /* (e) tally replies: a grant (drives to WON quorum on 3-node), then a + * duplicate of the same grant, an out-of-range peer, and a deny. */ + TEST_ASSERT_EQUAL_INT(RAFT_PRE_VOTE_WON, + raft_on_pre_vote_reply(&s, 1, 1 /* grant */)); + /* round closed after WON; further replies are no-ops on persistent state */ + (void)raft_on_pre_vote_reply(&s, 1, 1 /* duplicate grant */); + (void)raft_on_pre_vote_reply(&s, 99, 1 /* out-of-range */); + (void)raft_on_pre_vote_reply(&s, 2, 0 /* late deny */); + + /* INVARIANT: persistent Raft state byte-for-byte unchanged. */ + TEST_ASSERT_EQUAL_UINT64(term0, s.term); + TEST_ASSERT_EQUAL_INT(voted_for0, s.voted_for); + TEST_ASSERT_EQUAL_UINT64(voted_for_term0, s.voted_for_term); + TEST_ASSERT_EQUAL_INT(role0, s.role); + TEST_ASSERT_EQUAL_INT(RAFT_FOLLOWER, s.role); /* never promoted */ + + /* INVARIANT: PreVote never persists and never fires leadership callbacks. */ + TEST_ASSERT_EQUAL_INT(0, g_mock.persist_count); + TEST_ASSERT_EQUAL_INT(0, g_mock.become_leader_count); + TEST_ASSERT_EQUAL_INT(0, g_mock.become_follower_count); +} + +/* + * test_invariant_prevote_lost_sequence_pure_no_persist (Req 6.2, 1.4) + * + * Same purity property as above, but driving the round to the LOST terminal + * outcome (all peers deny). A WON path and a LOST path are the two ways a + * round can end; both must be side-effect-free. This guards the case where + * a frozen-then-resumed standby gets no PreVote majority (Req 4) — the round + * must leave term/vote/role untouched so the node simply re-attaches. + */ +static void test_invariant_prevote_lost_sequence_pure_no_persist(void) +{ + raft_state_t s; + raft_callbacks_t cbs = make_mock_cbs(); + + cbs.on_trace = mock_trace; + reset_mock(); + + TEST_ASSERT_EQUAL_INT(0, init_vote_node(&s, &cbs, 3, 0, 9)); + s.voted_for = 0; + s.voted_for_term = 9; + + const uint64_t term0 = s.term; + const int voted_for0 = s.voted_for; + const uint64_t voted_for_term0 = s.voted_for_term; + const raft_role_t role0 = s.role; + + TEST_ASSERT_EQUAL_INT(0, raft_begin_pre_vote(&s)); + + /* both peers deny → LOST, no majority */ + TEST_ASSERT_EQUAL_INT(RAFT_PRE_VOTE_PENDING, + raft_on_pre_vote_reply(&s, 1, 0)); + TEST_ASSERT_EQUAL_INT(RAFT_PRE_VOTE_LOST, + raft_on_pre_vote_reply(&s, 2, 0)); + + /* INVARIANT: persistent state unchanged across a LOST round. */ + TEST_ASSERT_EQUAL_UINT64(term0, s.term); + TEST_ASSERT_EQUAL_INT(voted_for0, s.voted_for); + TEST_ASSERT_EQUAL_UINT64(voted_for_term0, s.voted_for_term); + TEST_ASSERT_EQUAL_INT(role0, s.role); + TEST_ASSERT_EQUAL_INT(0, g_mock.persist_count); + TEST_ASSERT_EQUAL_INT(0, g_mock.become_leader_count); + TEST_ASSERT_EQUAL_INT(0, g_mock.become_follower_count); +} + +/* + * test_invariant_prevote_won_grants_no_leadership (Req 6.1) + * + * ELECTION SAFETY property: a PreVote round that reaches RAFT_PRE_VOTE_WON + * grants NO leadership. The node must remain RAFT_FOLLOWER and no + * on_become_leader / on_become_follower callback may fire — a PreVote WON is + * a STATUS the controller acts on, not a leadership transition. Only the + * separate, unchanged raft_start_election path creates a leader. + * + * The test then demonstrates the contrast: invoking the real + * raft_start_election (the only leadership-creating path) from the same + * still-FOLLOWER node bumps the term and self-votes — proving the leader is + * created exclusively by the real path, never by the PreVote WON itself. + */ +static void test_invariant_prevote_won_grants_no_leadership(void) +{ + raft_state_t s; + raft_callbacks_t cbs = make_mock_cbs(); + + reset_mock(); + /* arm a round on a 3-node FOLLOWER at term=5 (self-grant in progress) */ + TEST_ASSERT_EQUAL_INT(0, arm_pre_vote_round(&s, &cbs, 3, 0, 5)); + + const uint64_t term_before_won = s.term; + + /* one peer grant → WON on a 3-node cluster (quorum=2) */ + int rc = raft_on_pre_vote_reply(&s, 1, 1 /* grant */); + TEST_ASSERT_EQUAL_INT(RAFT_PRE_VOTE_WON, rc); + + /* INVARIANT (Election Safety): WON created NO leader. */ + TEST_ASSERT_EQUAL_INT(RAFT_FOLLOWER, s.role); /* still a follower */ + TEST_ASSERT_EQUAL_UINT64(term_before_won, s.term); /* term not advanced */ + TEST_ASSERT_EQUAL_INT(0, g_mock.become_leader_count); + TEST_ASSERT_EQUAL_INT(0, g_mock.become_follower_count); + TEST_ASSERT_EQUAL_INT(0, g_mock.persist_count); + + /* CONTRAST: leadership is created ONLY by the unchanged real path. + * Starting the real election now bumps the term + records the self-vote + * (this is the sole term-writing / leadership-creating transition). */ + reset_mock(); + TEST_ASSERT_EQUAL_INT(RAFT_OK, raft_start_election(&s)); + TEST_ASSERT_EQUAL_INT(RAFT_CANDIDATE, s.role); + TEST_ASSERT_EQUAL_UINT64(term_before_won + 1, s.term); /* real bump here */ + TEST_ASSERT_EQUAL_INT(1, g_mock.persist_count); /* persisted here */ +} + +/* + * test_invariant_real_vote_higher_term_adopt_unchanged (Req 5.2, 5.3) + * + * REAL-VOTE-PATH-UNCHANGED property: PreVote must not have altered the + * legitimate higher-term-adopt failover path that the bug-339/bug-340 fixes + * depend on. After running a full PreVote round on a node, the real + * raft_on_vote_request still adopts a strictly higher term and steps a + * leader down (fires on_become_follower), and raft_on_vote_reply still wins + * at quorum (fires on_become_leader) — exactly as before PreVote existed. + * + * This is the library-level guard for bug-339 (higher-term adopt on + * RDHUP failover) and bug-340 (rejoin), confirming PreVote sits beside the + * real-vote path without modifying it. + */ +static void test_invariant_real_vote_higher_term_adopt_unchanged(void) +{ + raft_state_t s; + raft_callbacks_t cbs = make_mock_cbs(); + uint64_t reply_term = 0; + + cbs.on_trace = mock_trace; + + /* --- Part 1: higher-term real RequestVote adopts term + steps down a + * leader, even after a PreVote round ran on this node. --- */ + reset_mock(); + TEST_ASSERT_EQUAL_INT(0, init_vote_node(&s, &cbs, 3, 0, 2)); + + /* Run a (lost) PreVote round first to prove it leaves the real-vote + * adopt path untouched. */ + TEST_ASSERT_EQUAL_INT(0, raft_begin_pre_vote(&s)); + (void)raft_on_pre_vote_reply(&s, 1, 0); + (void)raft_on_pre_vote_reply(&s, 2, 0); + TEST_ASSERT_EQUAL_UINT64(2, s.term); /* PreVote did not move the term */ + + /* Now this node is the leader in term 2 and a real higher-term vote + * request arrives — the unchanged Step 2 must adopt term 5 and step down. */ + s.role = RAFT_LEADER; + s.voted_for = 0; + s.voted_for_term = 2; + reset_mock(); + + int rc = raft_on_vote_request(&s, 1, 5, &reply_term); + + /* Higher-term adopt + leader step-down, exactly as bug-339/340 require. */ + TEST_ASSERT_EQUAL_UINT64(5, s.term); + TEST_ASSERT_EQUAL_INT(RAFT_FOLLOWER, s.role); + TEST_ASSERT_EQUAL_UINT64(5, reply_term); + TEST_ASSERT_EQUAL_INT(1, g_mock.become_follower_count); /* stepped down */ + TEST_ASSERT_EQUAL_INT(RAFT_GRANT, rc); /* then grants */ + + /* --- Part 2: real raft_on_vote_reply still elects a leader at quorum, + * unaffected by PreVote. --- */ + reset_mock(); + TEST_ASSERT_EQUAL_INT(0, init_node(&s, &cbs, 3, 0)); + s.role = RAFT_CANDIDATE; + s.term = 1; + s.votes_granted = 1; /* self-vote */ + s.replies_received = 0; + s.election_decided = 0; + + int rcr = raft_on_vote_reply(&s, 1, 1 /* grant */, 1); + TEST_ASSERT_EQUAL_INT(RAFT_BECAME_LEADER, rcr); + TEST_ASSERT_EQUAL_INT(RAFT_LEADER, s.role); + TEST_ASSERT_EQUAL_INT(1, g_mock.become_leader_count); /* real path elects */ +} + /* ---------- test_raft entry point ---------- */ void test_raft(void) @@ -3634,6 +3931,12 @@ void test_raft(void) RUN_TEST(test_pre_vote_reply_out_of_range_peer_ignored); RUN_TEST(test_pre_vote_reply_5node_won_at_three); + /* Raft safety-invariant assertions for the PreVote API (task 6.1, RN-1) */ + RUN_TEST(test_invariant_prevote_sequence_pure_no_persist); + RUN_TEST(test_invariant_prevote_lost_sequence_pure_no_persist); + RUN_TEST(test_invariant_prevote_won_grants_no_leadership); + RUN_TEST(test_invariant_real_vote_higher_term_adopt_unchanged); + /* simulator init (task 4.1) */ #ifdef XCE_TESTING RUN_TEST(test_sim_init_3node);