docs(raft-ha-core-safety): retarget Phase 4/5 to RDHUP-flap root cause

Phase-4/5 investigation found the live stall is a recovered standby with a
divergent uncommitted tail (former-primary shape) that never reconverges:
loops on ae_reject_logmismatch, its control channel flaps ~15s, each flap
spawns an unwinnable PreVote failover while a live primary exists.
- Phase 4 (Standby Reconvergence): lead with divergent-tail truncate+catch-up
  (make the AE backtrack + follower-conflict-truncate fire for a former-primary
  tail, not just a short suffix), keep the applied/log_len healthy gate.
- Phase 5 (Election Liveness): retarget from 'missing election-restart' (retry
  works) to spurious-failover suppression — reconnect+catch-up on transient
  RDHUP, don't storm unwinnable PreVotes while a current-term primary is
  reachable. 5.2 now _Depends 4.2_.
This commit is contained in:
Rongsong Shen 2026-06-28 03:24:12 +00:00
parent 8974f2cc97
commit 4fa04a852b
2 changed files with 29 additions and 21 deletions

View file

@ -260,19 +260,21 @@ A node is reported healthy/3-of-3 only when committed **and** applied state matc
#### Standby Reconvergence #### Standby Reconvergence
| Field | Detail | | Field | Detail |
|-------|--------| |-------|--------|
| Intent | Report a rejoining node healthy/3-of-3 only after committed **and** applied state match the leader. | | Intent | A recovered standby — including a former primary holding a divergent uncommitted tail above the new leader's committed point — reconverges to follower (truncates the divergent tail, catches up) and is reported healthy/3-of-3 only after committed **and** applied state match the leader. |
| Requirements | 5.1, 5.2, 5.3, 5.4 | | Requirements | 5.1, 5.2, 5.3, 5.4 |
**Responsibilities & Constraints**: post-recovery `log_len`/applied-lsn sync; complete outstanding catch-up apply before "healthy"; bounded recovery window. **Responsibilities & Constraints**:
- **Divergent-tail reconvergence (the live-stall fix, task 1.3/Phase-4 investigation):** when a standby recovers with an uncommitted tail whose entries conflict with the leader's log (the former-primary `current_lsn > leader_committed` shape — e.g. ctrl-2 holding 12-15 at an old term while the leader committed 11), the AE log-matching backtrack must reach the divergence point and the follower must **truncate the conflicting suffix** (follower-AE-conflict-truncate contract) and accept the leader's entries — the same way a short-suffix standby already reconverges (`ae_reject_logmismatch` ×N → `ae_already_have`). Determine and remove whatever prevents a longer/former-primary divergent tail from reaching `ae_already_have` (candidate: the leader's `next_index` backtrack does not cross the divergence before the control channel drops; or the recovered tip is advertised in a way that stalls the backtrack).
- Post-recovery `log_len`/applied-lsn sync; complete outstanding catch-up apply before "healthy"; bounded recovery window.
**Dependencies**: Inbound: rejoin path (P0). Outbound: Unified Entry Ingest (P0); `ha_rejoin_reconcile` hook (P1). **Dependencies**: Inbound: rejoin path (P0). Outbound: Unified Entry Ingest (P0); `ha_rejoin_reconcile` hook (P1); the leader-side AE streamer `next_index` backtrack (P0).
**Contracts**: State [x] / Service [x] **Contracts**: State [x] / Service [x]
- Postcondition: `applied_lsn == log_len == leader_committed_lsn` before reporting converged; otherwise remain `CatchingUp`. - Postcondition: a recovered standby with a divergent uncommitted tail truncates it and reaches `applied_lsn == log_len == leader_committed_lsn`; reported converged only then, otherwise `CatchingUp`.
**Implementation Notes** **Implementation Notes**
- Integration: reuse the `ha-convergence-recovery` rejoin hook; add the applied/log_len equality gate for the chaotic path. - Integration: reuse the `ha-convergence-recovery` rejoin hook; ensure the AE backtrack + follower-conflict-truncate path actually fires for a former-primary divergent tail, not only a 1-2 entry suffix.
- Validation: RED integration test — inject an apply gap and assert the node is not reported converged until the gap closes. - Validation: RED integration test — construct a recovered standby with a multi-entry divergent uncommitted tail above the leader's committed point and assert it reconverges to `ae_already_have` (no permanent `ae_reject_logmismatch` loop) and is not reported converged until applied state matches.
#### Election Liveness #### Election Liveness
| Field | Detail | | Field | Detail |
@ -280,15 +282,18 @@ A node is reported healthy/3-of-3 only when committed **and** applied state matc
| Intent | A member that loses its primary always proceeds to a completed election; at most one committing primary per term. | | Intent | A member that loses its primary always proceeds to a completed election; at most one committing primary per term. |
| Requirements | 4.1, 4.2, 4.3, 6.1, 6.2, 6.3 | | Requirements | 4.1, 4.2, 4.3, 6.1, 6.2, 6.3 |
**Responsibilities & Constraints**: on primary loss with quorum reachable, elect a higher-term primary within the failover window; restart a failed election round; step down on observing a higher/equal-term leader. No permanent stall under repeated rapid rounds. **Responsibilities & Constraints**:
- On *genuine* primary loss with quorum reachable, elect a higher-term primary within the failover window; restart a failed election round; step down on observing a higher/equal-term leader. No permanent stall under repeated rapid rounds.
- **Spurious-failover suppression (the live-stall fix, task 1.3/Phase-5 investigation):** a *transient* primary control-channel RDHUP must not launch an unwinnable PreVote-failover storm while a current-term primary is actually alive and reachable by the quorum. The observed stall: a recovered standby whose channel to the live primary flaps (~15s) treats each RDHUP as "primary died" → `ha_begin_failover` → PreVote that times out (peers see the primary alive, deny/ignore) → reconnect → repeat forever, so the node never rejoins. The fix: on a control-channel RDHUP, **attempt reconnect + catch-up first**, and/or back off failover when a node's own PreVotes repeatedly fail to reach a quorum because a current-term leader exists — only escalate to a real failover when the primary is genuinely unreachable to the quorum. The election *retry* already works (R6); the defect is retrying an unwinnable election instead of rejoining the live primary.
**Dependencies**: Inbound: failover detection (P0). Outbound: Raft vote/election + `raft_cb_vote_eligible` (P0). **Dependencies**: Inbound: failover detection / `ha_on_primary_ctrl_fd_rdhup` (P0). Outbound: Raft vote/election + `raft_cb_vote_eligible` (P0); peer reconnect path (P0).
**Contracts**: Service [x] **Contracts**: Service [x]
- Invariant: never two committing primaries in one term (Election Safety); a node without a primary keeps initiating elections (liveness). - Invariant: never two committing primaries in one term (Election Safety); a node without a *reachable* primary keeps initiating elections (liveness); a node WITH a reachable current-term primary rejoins it rather than launching repeated unwinnable failovers.
**Implementation Notes** **Implementation Notes**
- Validation (liveness, R6): RED integration test forces repeated rapid kill/restart rounds and asserts a higher-term `CTRL_PRIMARY` appears each round; a scripted single-round failure asserts a follow-on election starts. - Validation (liveness, R6): RED integration test forces repeated rapid kill/restart rounds and asserts a higher-term `CTRL_PRIMARY` appears each round; a scripted single-round failure asserts a follow-on election starts.
- Validation (spurious-failover, the live stall): RED test/soak asserts a recovered standby whose control channel flaps while a current-term primary is alive does NOT enter an unbounded `ha_begin_failover`/`PreVote timed out` loop — it reconnects and rejoins as follower.
- Validation (safety, R4 — two-leaders-per-term): an explicit **Election Safety assertion** runs in the chaotic harness and soak — for every observed term, at most one member ever reaches committing-primary state. This is a *falsifiable verification*, not an assertion of correctness: it maps to `raft/raft.tla` Election Safety and must hold under overlapping kills. If it fails, the design's "library already enforces single-leader" assumption is disproven and a concrete guard (e.g. tighten the pre-vote/vote-once window at the adapter promotion gate) becomes required work rather than verification. - Validation (safety, R4 — two-leaders-per-term): an explicit **Election Safety assertion** runs in the chaotic harness and soak — for every observed term, at most one member ever reaches committing-primary state. This is a *falsifiable verification*, not an assertion of correctness: it maps to `raft/raft.tla` Election Safety and must hold under overlapping kills. If it fails, the design's "library already enforces single-leader" assumption is disproven and a concrete guard (e.g. tighten the pre-vote/vote-once window at the adapter promotion gate) becomes required work rather than verification.
- Risks: over-eager step-down could itself cause a stall — step-down must be paired with election restart. The harness must distinguish a *liveness* failure (no primary) from a *safety* failure (two primaries) so a fix for one does not regress the other. - Risks: over-eager step-down could itself cause a stall — step-down must be paired with election restart. The harness must distinguish a *liveness* failure (no primary) from a *safety* failure (two primaries) so a fix for one does not regress the other.

View file

@ -81,31 +81,34 @@
- _Depends: 2.4_ - _Depends: 2.4_
- [ ] 4. Standby reconvergence completeness - [ ] 4. Standby reconvergence completeness
- [ ] 4.1 RED: reconvergence-gate test - _Root cause (Phase-4/5 investigation, `research.md`): a recovered standby holding a divergent uncommitted tail above the new leader's committed point (former-primary shape, e.g. ctrl-2 with 12-15 at an old term while leader committed 11) never reaches `ae_already_have` — it loops on `ae_reject_logmismatch`, its control channel flaps, and it never rejoins. A short-suffix standby (ctrl-3) DOES reconverge, so the backtrack works for small divergence but not the former-primary tail._
- Add a case where a rejoining node with an injected catch-up apply gap must not be reported converged/healthy until `applied_lsn` and `log_len` equal the leader's committed boundary (today the node is healthy at match-index alone) - [ ] 4.1 RED: divergent-tail reconvergence + apply-gap gate tests
- Observable completion: the case FAILS on the baseline because convergence is reported before applied-state agreement - Primary case: construct a recovered standby with a MULTI-entry divergent uncommitted tail above the leader's committed point and assert it reconverges to follower — truncates the conflicting suffix and reaches `ae_already_have` (no permanent `ae_reject_logmismatch` loop). Secondary case: a rejoining node with an injected catch-up apply gap must not be reported converged/healthy until `applied_lsn` and `log_len` equal the leader's committed boundary
- Observable completion: both cases FAIL on the baseline (the divergent-tail case loops on log-mismatch / never truncates; the apply-gap case reports healthy at match-index alone)
- _Requirements: 5.1, 5.2, 5.3, 5.4, 7.2_ - _Requirements: 5.1, 5.2, 5.3, 5.4, 7.2_
- _Boundary: Standby Reconvergence_ - _Boundary: Standby Reconvergence_
- [ ] 4.2 Gate healthy/3-of-3 on committed-and-applied agreement - [ ] 4.2 Make a divergent uncommitted tail truncate + catch up, and gate healthy on applied agreement
- Synchronize post-recovery `log_len`/applied-lsn and complete outstanding catch-up apply (routed through the seam, reusing the rejoin intake hook) before reporting a node converged; bound the recovery window - Ensure the AE log-matching backtrack + follower-AE-conflict-truncate path fires for a former-primary divergent tail (not only a 1-2 entry suffix) so the standby truncates the conflicting suffix and accepts the leader's entries; synchronize post-recovery `log_len`/applied-lsn and complete outstanding catch-up apply (routed through the seam, reusing the rejoin intake hook) before reporting converged; bound the recovery window
- Observable completion: 4.1 passes; a rejoining node reports converged only after `applied_lsn == log_len == leader committed`, restoring a healthy 3-of-3 - Observable completion: 4.1 passes; a recovered standby with a divergent uncommitted tail reconverges to `ae_already_have` and reports converged only after `applied_lsn == log_len == leader committed`, restoring a healthy 3-of-3
- _Requirements: 5.1, 5.2, 5.3, 5.4_ - _Requirements: 5.1, 5.2, 5.3, 5.4_
- _Boundary: Standby Reconvergence_ - _Boundary: Standby Reconvergence_
- _Depends: 2.4_ - _Depends: 2.4_
- [ ] 5. Election liveness and safety under churn - [ ] 5. Election liveness and safety under churn
- [ ] 5.1 RED: election liveness and Election Safety tests - _Root cause (Phase-4/5 investigation, `research.md`): the live stall is NOT a missing election-restart (retry works) — it is a recovered standby treating a TRANSIENT control-channel RDHUP as "primary died" and launching an UNWINNABLE PreVote-failover storm while a current-term primary is alive (peers deny/ignore, round times out, reconnect, repeat ~15s). The node retries an election it can never win instead of rejoining the live primary._
- Add cases: repeated rapid kill/restart rounds must yield a higher-term primary each round; a scripted failed election round must be followed by another election; across overlapping kills, at most one member ever reaches committing-primary per term (Election Safety, mapped to `raft/raft.tla`) - [ ] 5.1 RED: spurious-failover suppression + election liveness + Election Safety tests
- Observable completion: the liveness cases FAIL on the baseline (round-N stall); the Election Safety assertion runs and reports per-term primary counts - Primary case: a recovered standby whose primary control channel flaps (transient RDHUP) while a current-term primary is alive and quorum-reachable must NOT enter an unbounded `ha_begin_failover`/`PreVote timed out` loop — it reconnects and rejoins as follower. Liveness case: on GENUINE primary loss, repeated rapid kill/restart rounds yield a higher-term primary each round; a scripted failed round is followed by another election. Safety case: across overlapping kills, at most one member ever reaches committing-primary per term (Election Safety, mapped to `raft/raft.tla`)
- Observable completion: the spurious-failover case FAILS on the baseline (unbounded prevote-timeout loop while a live primary exists); the liveness cases pass/fail per the stall; the Election Safety assertion runs and reports per-term primary counts
- _Requirements: 4.1, 4.3, 6.1, 6.2, 6.3, 7.3_ - _Requirements: 4.1, 4.3, 6.1, 6.2, 6.3, 7.3_
- _Boundary: Election Liveness_ - _Boundary: Election Liveness_
- [ ] 5.2 Guarantee election completion without losing single-leader safety - [ ] 5.2 Suppress unwinnable failover on transient RDHUP; keep genuine-loss liveness and single-leader safety
- Ensure a failed election round triggers a further election (no permanent stall while quorum is reachable); pair step-down-on-higher-term with election restart; preserve at-most-one-committing-primary-per-term - On a control-channel RDHUP, attempt reconnect + catch-up first, and/or back off failover when a node's own PreVotes repeatedly fail to reach quorum because a current-term leader exists — only escalate to a real election when the primary is genuinely unreachable to the quorum. Preserve: genuine primary loss still elects a higher-term primary (no permanent stall while quorum reachable); step-down-on-higher-term paired with election restart; at-most-one-committing-primary-per-term
- Observable completion: 5.1 liveness cases pass with no permanent stall across rapid rounds; the Election Safety assertion still holds (no two committing primaries in a term) - Observable completion: 5.1 spurious-failover case passes (a recovered standby rejoins a live primary instead of prevote-spinning); genuine-loss liveness still completes each round; the Election Safety assertion still holds
- _Requirements: 4.1, 4.2, 4.3, 6.1, 6.2, 6.3_ - _Requirements: 4.1, 4.2, 4.3, 6.1, 6.2, 6.3_
- _Boundary: Election Liveness_ - _Boundary: Election Liveness_
- _Depends: 4.2_
- [ ] 6. Integration: single-seam invariant end-to-end - [ ] 6. Integration: single-seam invariant end-to-end
- [ ] 6.1 Verify leader→standby replication carries (term, payload) faithfully end-to-end - [ ] 6.1 Verify leader→standby replication carries (term, payload) faithfully end-to-end