forked from lei.chen/myxce
docs(raft-ha-core-safety): hypothesis-validation closeout (task 7.3)
Confirms the live chaotic soak eliminates the divergence this spec's Headline Finding hypothesized (LSN-9 committed-prefix divergence, round-4 election stall) -- not by synthetic unit tests alone, but by the task 7.2 acceptance soak (3 independent PASS runs, zero divergence, zero job loss, 6/6 clean elections). Documents the full resolution chain (Phase 2 payload loss -> Phase 5 election liveness, 5 layers -> Phase 3 snapshot boundary -> Phase 6 end-to-end + single-seam verification -> Phase 7.1 full regression sweep) and reviews the final behavior against all four raft/raft.tla safety invariants (Election Safety, Leader Completeness, State Machine Safety, Commit Ordering/Durability). No residual divergence remains open under this spec; two items explicitly routed to their owning specs rather than closed here (dormant heartbeat-driver path, soak harness's transient committedLsn=0 read). This closes the last task in raft-ha-core-safety (18/18 sub-tasks).
This commit is contained in:
parent
a525091b02
commit
2806a96c37
2 changed files with 78 additions and 1 deletions
|
|
@ -911,3 +911,80 @@ window (not just the instantaneous role check). Must preserve genuine-loss liven
|
|||
re-introduce the stall 5.2/5.5/5.6/5.7 fixed. Needs a deterministic repro: a dead-primary RDHUP
|
||||
cadence + 2 survivors → assert bounded term growth (≤ K bumps) to convergence. Stochastic in the
|
||||
soak (1 of 2 ten-round runs). Tracked as 5.10(b).
|
||||
|
||||
## Task 7.3 — Hypothesis-validation closeout (2026-07-01)
|
||||
|
||||
**Original hypothesis (Headline Finding, above):** the `(term,lsn)` commit-identity machinery
|
||||
already existed at baseline, but the live chaotic soak still diverged — `walcompare FAIL:
|
||||
committed-prefix divergence at LSN 9` (round 3) — so this spec was scoped as a residual-defect +
|
||||
convergence/liveness + live-verification spec, not a from-scratch build.
|
||||
|
||||
**Resolution chain, in the order landed:**
|
||||
- **Payload loss (Phase 2, done 2026-06-27):** cross-term catch-up streamer silently shipped
|
||||
`PLEN=0` on a short `pread`/`malloc`-fail (task 2.4); persist guard hardened to
|
||||
`(term,lsn,payload-crc)` (task 2.2). Closed the LSN-9 divergence signature from the Headline
|
||||
Finding.
|
||||
- **Election liveness (Phase 5, done 2026-06-30/07-01):** five layers peeled on the round-4 stall
|
||||
— spurious-failover suppression (5.2), lagging-survivor eligibility deadlock (5.3), an upstream
|
||||
ABBA deadlock + release SIGSEGV (5.4, routed to `raft-drive-async`), advertised-term cross-deny
|
||||
(5.5), dueling-candidate split-vote (5.6), vote-reply term-lag resonance (5.7), an
|
||||
endpoint-teardown UAF (5.8), and the hook-rc-clobber committed-job-loss bug (5.9, bug-1306).
|
||||
Each was root-caused to a concrete site before any fix, per this spec's own discipline.
|
||||
- **Committed-divergence residual (5.10a) + snapshot boundary (Phase 3, done 2026-07-01):** the
|
||||
last standing divergence source was a member that caught up via full-checkpoint snapshot —
|
||||
`ha_handle_snapshot_chunk`/`persist_load_snapshot` advanced `checkpoint_lsn`/`current_lsn`/
|
||||
`applied_lsn` but never reconciled a *term* at the checkpoint boundary, so a stale local term
|
||||
from a divergent pre-snapshot entry survived install unrepaired (task 3.1 RED: `Expected 7 Was
|
||||
3`). Fixed in task 3.2 by carrying the checkpoint's term on the wire (`SnapshotTransfer.
|
||||
checkpointTerm`, append-only field) and reconciling it into the receiver's per-LSN term index
|
||||
on install, before `applied_lsn` advances.
|
||||
- **End-to-end + single-seam verification (Phase 6, done 2026-07-01):** task 6.1 proved the
|
||||
(term,payload) fidelity guarantee holds across two real `persist_t`/WAL instances through the
|
||||
real production ingest seam, for both live replication and cross-term catch-up. Task 6.2
|
||||
confirmed the one remaining term-blind direct-persist path (`ha_apply_single_entry`) is
|
||||
unreachable with a real non-zero term in any current production path (its sole trigger,
|
||||
`raft_send_append_entries`, has zero production call sites) — documented safe-by-guard rather
|
||||
than speculatively retired, and pinned that `(term,lsn)` identity survives a restart (`replay_wal`
|
||||
already reconstructs the term index via `record_entry_term`).
|
||||
- **Full regression sweep (task 7.1, done 2026-07-01):** the first-ever full 69-group ASAN sweep
|
||||
of `controller_unit_test` (previously only run suite-by-suite in fragments) surfaced exactly 2
|
||||
stale tests — both asserting a PRE-fix contract that an earlier, already-approved task in this
|
||||
same spec (5.3's PreVote-gate relaxation; 5.9's hook-to-explicit-commit-barrier extraction) had
|
||||
deliberately superseded. Fixed test-only; 69/69 groups green, 0 ASAN reports.
|
||||
|
||||
**Live soak closure (task 7.2, done 2026-07-01):** a ≥6-round chaotic (overlapping-kill) soak
|
||||
against real-fs release binaries built from the full fix chain above — `committed_divergence=0`,
|
||||
`committed_job_loss=0`, 3-of-3 reconvergence and a new primary elected every round (terms
|
||||
2→4→5→6→7→8→9, monotonic, no stalls), independently reproduced 3 times (implementer, adversarial
|
||||
reviewer, and once more after a harness-hardening pass that replaced a static
|
||||
`1+2*njobs` divergence-boundary estimate — which had produced a spurious `divergence=7` on a
|
||||
provably byte-identical WAL set, per `waldump` forensics — with the live authoritative
|
||||
`committedLsn`, gated on genuine cluster convergence). **The hypothesis is confirmed resolved by
|
||||
the live soak, not by synthetic unit tests alone**, satisfying this task's own bar.
|
||||
|
||||
**`raft/raft.tla` invariant review against final behavior:**
|
||||
- **Election Safety** (≤1 leader/term): held throughout every soak round — `probe_primary`
|
||||
reported one committing primary at each of the 7 distinct terms observed; task 5.3's PreVote
|
||||
eligibility gate and the vote-once-per-term contract (unchanged by this spec, exercised
|
||||
end-to-end by the live soak) are the enforcing mechanism.
|
||||
- **Leader Completeness** (committed entries survive election): the promotion truncate clamp
|
||||
(`max(safe_committed_lsn, durable_tip)`, bug-1060) was never triggered to cut a leader's own
|
||||
durable log in any soak round; task 3.2's snapshot-boundary reconcile closes the one path
|
||||
(post-snapshot-install AE intake) that previously lacked a verifiable `(term,lsn)` anchor to
|
||||
check completeness against.
|
||||
- **State Machine Safety** (no divergent committed entries): `walcompare` reported zero divergence
|
||||
across all three post-hardening soak runs; `waldump` forensics on the pre-hardening run
|
||||
independently confirmed byte-identical, gap-free, CRC-intact WALs across all 3 members — the
|
||||
one observed "divergence" was a harness measurement artifact, not a state-machine-safety
|
||||
violation, and the harness itself is now fixed (task 7.2).
|
||||
- **Commit Ordering / Durability** (contiguous prefix, ack ⇒ durable-on-majority): unaffected by
|
||||
this spec's changes (owned by `ha-commit-durability`/`raft-apply-decoupling`); indirectly
|
||||
reconfirmed by zero committed-job loss and gapless WAL chains across every soak round.
|
||||
|
||||
**Closure:** no residual divergence remains open under this spec. Two items are explicitly
|
||||
NOT part of this closure and are tracked to their owning specs, per this spec's established
|
||||
upstream-routing discipline: (1) the dormant `raft_send_append_entries`/heartbeat-driver path
|
||||
flagged in task 6.2 as a re-evaluation trigger for any future task that wires it up; (2) the soak
|
||||
harness's `probe_primary`/`ctrlstatus` transient `committedLsn=0` read (guarded against in task
|
||||
7.2, root cause of the transient read itself not further chased — the guard is sufficient for the
|
||||
harness's correctness and the transient does not affect production behavior).
|
||||
|
|
|
|||
|
|
@ -208,7 +208,7 @@
|
|||
- _Depends: 1.5, 6.2, 5.2, 5.3, 5.4_
|
||||
- _Blocked on bug-1283 (the round-4 stall had TWO independent causes). (1) bug-1282 — an ABBA lock-order deadlock in `src/lib` async dispatch (`io_worker` ep->lock→q->lock vs `vdispatcher` `dataq_deq` q->lock→ep->lock via `endpoint_is_task_blocked`) — is **FIXED** (commit 25e741d: `endpoint_t.busy` → `_Atomic int`, lockless; verified zero `__lll_lock_wait` post-fix; unit suite green). (2) bug-1286 — a SEPARATE release-only SIGSEGV on a restarted standby at round 4 (deadlocks hang, they don't crash) — is now **ROOT-CAUSED** (via the new `/xce-build debug` non-ASAN `-O0 -g3` profile + gdb): `myreq_handler` (cluster.c:251) does `c = ep->owner` then `ha_dispatch_gate(&c->ha, …)`; on a chaotic restart a `walCatchupEntry` (op 37) vtask runs with `ep->owner == NULL`, so `&c->ha == 0x3ff0` → deref crash at ha.c:3194. Fix = NULL-guard `c = ep->owner` in `myreq_handler` (+ ensure owner is set at accept time / not cleared mid-flight). is **FIXED** (commit 5db734a: NULL-guard `c = ep->owner` in myreq_handler). With BOTH bug-1282 and bug-1286 fixed, the round-4 soak shows NO crash / NO deadlock / NO fdatasync — but still stalls on a THIRD, now-unmasked cause: **task 5.5** — a pure election-liveness cross-deny (the freshest survivor is denied on eligibility because the other survivor still believes its dead primary is alive). 5.5 (advertised-term) is FIXED (b8453b2, verified: fresher survivor now wins PreVote + enters real election); 5.6 (don't preempt an in-flight election) is FIXED (81cb09a, unit-verified, reduces churn); the remaining 7.2 blocker is now **task 5.7** — vote-reply term-lag / unbounded term escalation under cold-connection churn (the freshest survivor is granted but its term out-races the grant). Consensus safety (Phase-2/5.2/5.3) is sound; elections + job safety hold for every round that completes. Separately, the soak over-counts divergence (boundary `1+2*njobs` vs primary `committedLsn`). Detail in `research.md` §"Both fixes verified". Re-run 7.2 after 5.5 lands._
|
||||
|
||||
- [ ] 7.3 Hypothesis-validation closeout
|
||||
- [x] 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_
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue