myxce/.kiro/specs/raft-ha-core-safety/tasks.md

Implementation Plan: raft-ha-core-safety

TDD (project steering, mandatory): every implementation sub-task is preceded by a testsuite sub-task that lands failing (RED) tests first, then implements to GREEN. The deterministic harness (Phase 1) is the RED infrastructure that pins every later fix to a walcompare/invariant violation. No (P) markers: Phases 2–6 all modify ha.c (and persist.c), and the RED cases share test_ha_core_safety.c, so the plan is sequential — concurrent edits would contend on the same files (same constraint as ha-convergence-recovery). Foundation Phase 1 establishes shared prerequisites and is also sequential. Correctness oracle: verify every change against raft/raft.tla and the invariant checklist in src/controller/CLAUDE.md (Election Safety, Leader Completeness, State Machine Safety, Commit Ordering/Durability). Verify anchors before editing (files drift): the design and research.md carry 2026-06-27 file:line anchors; re-grep before each edit. Hypothesis discipline: the term-blind bypass is the primary hypothesis, not proven sole cause. Task 1.3 must reproduce the live divergence first; a green synthetic unit test over a still-red soak does not satisfy 1.1/8.1.

• 1. Foundation: deterministic chaotic harness and live-divergence reproduction

• 1.1 Extend the divergence detector to a machine-checkable per-member report

  • Extend walcompare to emit a parseable per-member (lsn -> term, payload-crc, present/MISSING) report over the committed prefix, and classify each divergence as committed vs uncommitted
  • Observable completion: walcompare prints a parseable per-member report and a committed-vs-uncommitted classification; the existing soak still detects the round-3 LSN divergence through it
  • Requirements: 7.1, 7.5
  • Boundary: Deterministic Chaotic Harness

• 1.2 Add a chaotic soak mode with an isolated verdict

  • Add an overlapping-kill mode to the soak driver (kills landing inside election windows, not only sequential kill→wait→rejoin); produce a verdict that counts walcompare divergences and committed-job loss while excluding client-discovery (bug-854) and overlayfs fdatasync (bug-924) failures from the divergence/job-loss result
  • Observable completion: the soak runs chaotic mode against real-fs release binaries and emits a verdict whose divergence/job-loss counts are unaffected by bug-854/bug-924
  • Requirements: 7.5, 8.4
  • Boundary: Acceptance Soak Gate, Deterministic Chaotic Harness

• 1.3 Reproduce and classify the live divergence, then bisect to a seam

  • Run the chaotic soak to capture the actual walcompare committed-prefix divergence (RED), classify it via (term, lsn, pcrc) (which member, which term, committed vs uncommitted), and bisect it to the concrete ingest path; confirm or refute the term-blind-bypass hypothesis
  • Observable completion: a recorded RED divergence with member/term/lsn classification and the identified seam, written to research.md; the hypothesis is confirmed or a new trigger is named before any fix
  • Requirements: 7.1, 1.1
  • Boundary: Deterministic Chaotic Harness

• 1.4 Stand up the unit/integration harness infrastructure

  • Create test_ha_core_safety.c with the deterministic gate/probe seams (no sleeps; teardown drains pending delaymgr tasks to avoid the bug-1224 teardown-race UAF), the (term, lsn)/apply-gap/kill-injection fixtures, and register it in the controller unit-test build; include one smoke-RED case proving the harness can observe a divergence. The per-defect RED bodies are owned by their phases (2.3 ingest, 4.1 reconvergence, 5.1 election) — this task provides the shared seams they build on, not those cases
  • Observable completion: test_ha_core_safety builds and runs, the injection fixtures and probe seams are usable by later phases, and the smoke-RED case FAILs on the baseline with no ASAN teardown errors
  • Requirements: 7.1, 7.4
  • Boundary: Deterministic Chaotic Harness

• 2. Committed-prefix divergence fix: persistence conflict guard and single-seam ingest

• 2.1 RED: persistence (term, lsn)-conflict tests

  • Add cases: a wrong-term entry written at an LSN followed by the correct term-carrying entry must end with the leader's term (today the LSN-only idempotency guard silently no-ops); a conflicting entry below local durable_tip must be truncatable; a matching entry must never be truncated
  • Observable completion: the new persistence cases FAIL on the baseline because the guard is LSN-only and silently skips the corrective write
  • Requirements: 1.1, 1.2, 2.1, 2.2, 3.1, 3.4
  • Boundary: Persist Conflict Guard

• 2.2 Make the persistence guard (term, lsn)-conflict-aware

  • Replace the LSN-only idempotency check: same LSN + same term is an idempotent no-op; same LSN + different term is surfaced as a conflict for the seam to truncate-then-repersist (never a silent no-op); never persist a non-leader term for a live-replicated entry; preserve persist-before-ACK and the term index
  • Observable completion: the 2.1 cases pass; the WAL at a re-written LSN holds exactly the leader's (term, payload); persist-before-ACK behavior unchanged
  • Requirements: 1.1, 1.2, 2.1, 2.2, 3.1
  • Boundary: Persist Conflict Guard

• 2.3 RED: single-seam ingest and unrecoverable-fence tests

  • Add cases asserting that every replicated/catch-up entry — including a term==0-shaped legacy entry — passes through the reconcile seam (logOk + conflict-truncate + leader-term stamp) and is reconciled, with no direct-persist bypass branch remaining; and a case where a node that cannot obtain the majority-agreed committed prefix takes the loud non-promotable fence and refuses promotion instead of serving divergent committed state
  • Observable completion: the ingest cases FAIL on the baseline because the term-blind branch bypasses the seam; the fence case FAILs because no unrecoverable-divergence fence exists yet
  • Requirements: 1.2, 3.2, 3.3, 7.1
  • Boundary: Unified Entry Ingest

• 2.4 Collapse the term-blind ingest path into the single reconcile seam

  • Route batch/single/catch-up ingest through raft_on_append_entries_request; retire the direct-persist branch; apply the follower-AE-conflict-truncate contract (logOk-gated, no promotion clamp) so a conflicting entry is repaired regardless of local durable_tip; surface genuinely-unrecoverable divergence as a loud non-promotable fence (never self-terminate); defer file I/O/truncation to delaymgr (never the callback/iomgr thread)
  • Observable completion: 2.3 passes (including the fence case — an unrepairable node refuses promotion and stays alive retrying); an injected divergent (term, lsn) is repaired through the seam; walcompare is clean on the 1.3 reproduction path
  • Requirements: 1.1, 1.2, 1.3, 2.1, 2.3, 3.1, 3.2, 3.3, 3.4
  • Boundary: Unified Entry Ingest
  • Depends: 2.2

• 3. Snapshot-boundary reconciliation

• 3.1 RED: snapshot post-install reconcile test

  • Add a case where a divergent pre-snapshot entry must be reconciled against the installed checkpoint's (term, lsn) boundary (today snapshot install sets applied-lsn without a (term, lsn) reconcile)
  • Observable completion: the case FAILS on the baseline because no (term, lsn) reconcile occurs at the snapshot boundary
  • Requirements: 3.1, 5.1
  • Boundary: Snapshot Boundary Reconcile

• 3.2 Establish the snapshot (term, lsn) boundary

  • Make snapshot install establish a verifiable (term, lsn) at the checkpoint so post-install AE intake reconciles correctly and no committed entry below the checkpoint can diverge
  • Observable completion: 3.1 passes; a member that installed a snapshot matches the leader's (term, payload-crc) at and below the checkpoint boundary
  • Requirements: 3.1, 5.1
  • Boundary: Snapshot Boundary Reconcile
  • Depends: 2.4

• 4. Standby reconvergence completeness

• 4.1 RED: reconvergence-gate test

  • 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)
  • Observable completion: the case FAILS on the baseline because convergence is reported before applied-state agreement
  • Requirements: 5.1, 5.2, 5.3, 5.4, 7.2
  • Boundary: Standby Reconvergence

• 4.2 Gate healthy/3-of-3 on committed-and-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
  • Observable completion: 4.1 passes; a rejoining node 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
  • Boundary: Standby Reconvergence
  • Depends: 2.4

• 5. Election liveness and safety under churn

• 5.1 RED: election liveness and Election Safety tests

  • 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)
  • Observable completion: the liveness cases FAIL on the baseline (round-N 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
  • Boundary: Election Liveness

• 5.2 Guarantee election completion without losing 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
  • 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)
  • Requirements: 4.1, 4.2, 4.3, 6.1, 6.2, 6.3
  • Boundary: Election Liveness

• 6. Integration: single-seam invariant end-to-end

• 6.1 Route live leader replication and catch-up streaming through the seam only

  • Ensure the leader-side streamer always emits term-carrying entries (no term==0 on the wire from a live leader) and the walAck catch-up continuation feeds only the seam ingest path
  • Observable completion: live leader replication carries the leader's term end-to-end; no term-0 entries reach a standby from a live leader; streamed catch-up entries reconcile through the seam
  • Requirements: 2.1, 2.3, 3.2
  • Boundary: Unified Entry Ingest, Persist Conflict Guard
  • Depends: 2.4

• 6.2 Verify the single-seam invariant and restart identity

  • Assert no ingest path (live replication, catch-up batch, snapshot post-install, rejoin) writes the WAL outside the reconcile seam, and that each entry's (term, lsn) identity survives a restart/recovery
  • Observable completion: an integration test confirms every ingest path reconciles through the seam and that entry terms are preserved across restart; no direct-persist bypass remains
  • Requirements: 1.1, 1.2, 2.4, 3.1
  • Depends: 2.4, 3.2, 4.2

• 7. Validation: regression and acceptance soak gate

• 7.1 Full controller suite under ASAN with the new harness green

  • Build and run the full controller unit suite under ASAN (suite-by-suite if the aggregate hits the known 300s cap); fix any regression from the ingest/persist/election changes
  • Observable completion: the full suite is green under ASAN and every test_ha_core_safety case passes with no ASAN errors
  • Requirements: 7.4
  • Depends: 6.2, 5.2

• 7.2 Acceptance chaotic-failover soak gate

  • Run the chaotic soak (≥6 rounds, overlapping kills) against real-fs release binaries and assert zero walcompare divergence, zero committed-job loss, and 3-of-3 reconvergence plus a new primary after every kill round, with bug-854/bug-924 isolated from the verdict
  • Observable completion: the soak exits PASS over ≥6 chaotic rounds with zero divergence and zero job loss — the green result that gates the raft-drive-async production flag-flip
  • Requirements: 1.4, 7.4, 8.1, 8.2, 8.3, 8.4
  • Depends: 6.2, 5.2

• 7.3 Hypothesis-validation closeout

  • Confirm the live soak divergence is eliminated by the implemented fixes (not by synthetic unit tests alone); if any residual divergence remains, classify it via walcompare (term, lsn, pcrc), record the new finding in research.md, and add a follow-up fix task rather than declaring closure
  • Observable completion: the soak divergence count is zero with closure justified by the live soak, OR a recorded new finding plus a follow-up task; raft/raft.tla invariants (Election Safety, Leader Completeness, State Machine Safety, Commit Ordering) reviewed against the final behavior
  • Requirements: 1.1, 1.4, 7.1, 8.1
  • Depends: 7.2