spec(ha-commit-durability): REOPEN for bug-795 total-outage cold-restart-all committed-job loss

Phase 6 added (6.1 reproduce-on-real-fs gates 6.2 root-cause / 6.3 fix / 6.4 revalidate).
Surfaced by the xce-test-e2e-primitives cold-restart-all soak step; Phase 5 only
validated rolling single-node failover. CLAUDE.md durability claim qualified pending 6.x.
This commit is contained in:
Rongsong Shen 2026-06-20 00:33:18 +00:00
parent aa615a184a
commit 3ad646ad0e
4 changed files with 249 additions and 1 deletions

View file

@ -78,7 +78,7 @@ The file `raft/raft.tla` contains Diego Ongaro's TLA+ specification of the Raft
**Commit Ordering** (contiguous, in log order — RULE): `committed_lsn` advances only as a contiguous prefix in LSN/append order; entries are never committed or reordered out of log order. The single-writer append lock (`p->lock`) is the serialization point. Durability flushing (incl. group-commit batching) makes a contiguous **prefix** durable only — `durable_lsn` is a prefix watermark, never a per-entry set, so a later entry can never be durable while an earlier one is not. Log order must preserve **causal dependencies** (append a cause before its effect — e.g. job submit before job start); independent concurrent events take an arbitrary but consistent total order, which is linearizable via the single serialization point plus commit-gated reply. Out-of-order / parallel commit is NOT supported by this single-log architecture (it would require per-entity logs with dependency tracking — explicitly out of scope).
**Commit Durability** (acknowledged ⇒ durable on a majority — GUARANTEED): when the controller replies success to a client, the operation's entry is `fdatasync`'d on a fault-tolerant majority (the acking member + ⌊N/2⌋ others); a member counts toward the commit majority for an LSN only once that LSN is durable locally (self caps at `durable_lsn`, not the appended tip). **CLOSED — bug-661, spec `ha-commit-durability` (landed 2026-06-18).** Mechanisms: `majority_candidate_locked` caps the primary self-contribution at `persist_durable_lsn` (not `highest_appended_lsn`); `fsync_worker` is a demand-driven group-commit flusher that advances `durable_lsn` only after a successful `fdatasync` and wakes the commit eval (fail-loud rc-gate — `durable_lsn` never advances on `fdatasync` error); the standby `fdatasync`s before its WalAck and the ACK is gated on that sync's success; recovery distinguishes a clean vs corruption-truncated WAL (`recover_verdict_t`) and re-derives the durable floor (WAL tip); the vote/PreVote freshness floor and a candidate's advertised position are durable-backed (candidate advertises bare `persist_durable_floor`, voter floor = `max(durable_floor, last_known_committed_lsn)`), and a pre-promotion gate fences a recovery-truncated/behind member (it catches up before leading; if genuinely unrecoverable it stays a loud, non-promotable, *alive* fence — never self-exits — and self-heals on peer return). Verified by unit/integration tests (2.x, 5.1), the deterministic ack-before-fdatasync gap E2E (RED→GREEN), and the rolling-failover soak (zero acked-job loss, cluster stays available) — NOT by `raft.tla`, which assumes a durable log (restores `log` intact from stable storage on restart, `raft.tla:165-174`) and so cannot model the durability invariant; that invariant rests on these tests + this checklist.
**Commit Durability** (acknowledged ⇒ durable on a majority — GUARANTEED): when the controller replies success to a client, the operation's entry is `fdatasync`'d on a fault-tolerant majority (the acking member + ⌊N/2⌋ others); a member counts toward the commit majority for an LSN only once that LSN is durable locally (self caps at `durable_lsn`, not the appended tip). **CLOSED — bug-661, spec `ha-commit-durability` (landed 2026-06-18).** Mechanisms: `majority_candidate_locked` caps the primary self-contribution at `persist_durable_lsn` (not `highest_appended_lsn`); `fsync_worker` is a demand-driven group-commit flusher that advances `durable_lsn` only after a successful `fdatasync` and wakes the commit eval (fail-loud rc-gate — `durable_lsn` never advances on `fdatasync` error); the standby `fdatasync`s before its WalAck and the ACK is gated on that sync's success; recovery distinguishes a clean vs corruption-truncated WAL (`recover_verdict_t`) and re-derives the durable floor (WAL tip); the vote/PreVote freshness floor and a candidate's advertised position are durable-backed (candidate advertises bare `persist_durable_floor`, voter floor = `max(durable_floor, last_known_committed_lsn)`), and a pre-promotion gate fences a recovery-truncated/behind member (it catches up before leading; if genuinely unrecoverable it stays a loud, non-promotable, *alive* fence — never self-exits — and self-heals on peer return). Verified by unit/integration tests (2.x, 5.1), the deterministic ack-before-fdatasync gap E2E (RED→GREEN), and the rolling-failover soak (zero acked-job loss, cluster stays available) — NOT by `raft.tla`, which assumes a durable log (restores `log` intact from stable storage on restart, `raft.tla:165-174`) and so cannot model the durability invariant; that invariant rests on these tests + this checklist. **CAVEAT — UNDER INVESTIGATION (bug-795, ha-commit-durability REOPENED 2026-06-19):** the verification above covers **rolling single-node failover**. A new **total-cluster-outage (cold-restart-all: kill ALL members + restart)** test (added by the `xce-test-e2e-primitives` soak) NON-DETERMINISTICALLY lost a committed job on an overlayfs sandbox (recovery logged WAL `truncate`). Real-durability-gap vs overlay-`fdatasync` artifact is being resolved by `ha-commit-durability` Phase 6 (6.1 reproduce-on-a-real-fs first). Until 6.x closes, treat the guarantee as **proven for rolling failover; pending confirmation under simultaneous total outage**.
### Post-Election Safe Commit Point (Critical)