myxce/.kiro/specs/ha-commit-durability/design.md
2026-08-10 17:51:51 +08:00

65 KiB
Raw Blame History

Design Document — ha-commit-durability

Overview

Purpose: Make acknowledgment imply durability in the XCE HA controller. Before this spec, the controller advanced its commit position on a majority of replication acknowledgments, but the primary counted its own contribution from a page-cache write (commit.c:majority_candidate_locked used highest_appended_lsn), while background fdatasync ran on a timer (fsync_worker). A "committed" operation could therefore be durable on as few as one member — bug-661, observed as permanent job loss across failover. (Post-implementation, majority_candidate_locked caps the self-contribution at persist_durable_lsn(ce->p) — verified current in src/controller/commit.c.)

Users: Cluster operators and every client whose acknowledged job/queue/worker operations must survive controller failover.

Impact: Strengthens the meaning of "committed" from "majority-ACKed (volatile)" to "persisted to stable storage on a fault-tolerant majority." The client reply path is already gated on the commit barrier, so once committed_lsn implies a durable majority, the invariant holds with no change to the reply path. Durability becomes group-commit: fsync_worker is repurposed from a fire-and-forget timer into a demand-driven flusher that, on append, batches fdatasync across all pending entries, advances durable_lsn, and wakes the commit evaluation. The commit majority counts durable_lsn (not appended). This amortizes one fdatasync across many entries — important because the highest-volume WAL traffic is WAL_MODE_RETAIN facts (job start/finish/fail/rusage), which are not client-latency-bound but must be durable before committed_lsn passes them. A second concern — a member with a corrupt or truncated log becoming authoritative — is closed by a recovery-integrity verdict and a promotion fence.

Goals

  • Durable commit: when the controller replies ok, the operation's log entry is fdatasync'd on the acknowledging member plus ⌊N/2⌋ others (Req 1).
  • Recovery integrity & promotion fence: a member that cannot reconstruct its committed state, or that lags the cluster's committed high-water mark, is barred from leadership until caught up — fail-loud when it cannot recover safely (Req 2).
  • Deterministic verification: durability timing is controllable in a test mode so the guarantee is provable without racing the clock (Req 3).
  • Preserve cluster liveness: durability work never stalls heartbeat/election processing.

Non-Goals

  • Single-record job-array persistence (job-array-single-wal-record, roadmap) — complements this spec by bounding per-array fsync count; independent of the group-commit flusher introduced here.
  • Per-entry synchronous fsync as the steady-state mechanism — superseded by group-commit (decision: the high-volume WAL_MODE_RETAIN path needs batching; see Components/DurableCommit).
  • Replication/ACK wire format (ha-wal-replication), per-entry majority arithmetic (ha-commit-engine), demotion truncate / rejoin reconciliation of an intact log (ha-convergence-recovery), promotion no-op / own-term gate (ha-single-leader-role), raw vote-grant arithmetic (raft-library).

Boundary Commitments

This Spec Owns

  • The durability precondition on the commit majority: a member contributes to the commit majority for an LSN only once that LSN is fdatasync'd locally. Introduces and is authoritative for persist_t.durable_lsn.
  • Group-commit durability: fsync_worker repurposed from a timer into a demand-driven flusher that batches fdatasync, advances durable_lsn, and wakes commit evaluation; persist_wal_async signals the flusher instead of deferring to a timer. Benefits all members on the high-volume WAL_MODE_RETAIN path.
  • Recovery integrity verdict: replay_wal/persist_recover distinguish a clean log end from a corruption-truncated end, and re-derive the member's durable floor from the recovered WAL.
  • Promotion eligibility fence: a recovery-truncated member, or one whose durable position is below the cluster committed high-water mark, is ineligible to become primary until caught up; re-eligible on catch-up.
  • Durable-backed freshness advertisement: a candidate's advertised log position and a voter's freshness floor derive from durable WAL state, not from volatile in-memory positions that survive a truncating restart.
  • Durability verification seam: a configurable durability cadence / background-flush control plus an XCE_TESTING hook.

Out of Boundary

  • Counting the majority or advancing committed_lsn arithmetic (ha-commit-engine — consumed; this spec changes only the durability precondition of its inputs).
  • The reply ordering / classification sweep (ha-commit-barrier-rollout — reused unchanged).
  • Demotion truncate + self-restart and rejoin reconciliation of an intact log (ha-convergence-recovery). This spec fences promotion; convergence-recovery handles demotion and rejoin.
  • Vote-grant arithmetic and term handling (raft-library); this spec adds only the durability/high-water precondition to the existing freshness gate.
  • WAL group-commit batching; job-array single-record persistence.

Allowed Dependencies

  • ha-commit-engine: commit_engine_t, commit_submit, majority_candidate_locked (modify self-contribution input only).
  • ha-wal-replication: standby ACK path (persist_wal_write_replicated) and catch-up streaming (consumed; in_catch_up reused).
  • ha-commit-barrier-rollout: persist_commit_barrier reply gate (consumed unchanged).
  • persist_t internals (current_lsn, committed_lsn, last_crc, segment I/O), ha_state_t (applied_lsn, last_known_committed_lsn, in_catch_up, term).
  • Constraint: must not write/persist committed_lsn to disk (Raft keeps the commit index volatile); durability is about the log, not the commit index.

Revalidation Triggers

  • Change to the durable_lsn semantics or to majority_candidate_locked's self-contribution → re-check ha-commit-engine and ha-convergence-recovery (which assume durable committed state).
  • Change to the promotion-eligibility gate or freshness-floor source → re-check ha-single-leader-role, ha-prevote, raft-library, and the CLAUDE.md TLA+ checklist.
  • Removal of fsync_worker → re-check any caller that assumed deferred fsync (audit wal_classify).
  • New wal_sync override surface → re-check main.c flag conventions and deployment scripts.

Architecture

Existing Architecture Analysis

  • Commit gate already off the iomgr thread: the AFTER_EVENT hook fires before the reply and persist_commit_barrier → commit_submit(COMMIT_MODE_WAIT) blocks on a condvar (job.c:2214, do_jobcontrol_op; AFTER_EVENT hook itself e.g. job.c:2189). (Note: citation corrected — file has grown substantially since this spec closed; original cited job.c:568-569.) Adding fdatasync to this path is liveness-safe.
  • Standby already persists-before-ACK: persist_wal_write_replicated fdatasyncs before returning (persist.c:1417, function defined at persist.c:1193). The primary is the asymmetric gap. (Note: citation corrected from the original persist.c:515.)
  • Recovery is silent-truncating: replay_wal (persist.c:4624) breaks on CRC chain break / mismatch / short read (now around persist.c:4704-4784, several distinct break sites) and returns a verdict; persist_recover never sets committed_lsn (stays 0). (Note: citation corrected — original cited persist.c:1021/1050/1042; replay_wal has since moved substantially within the file.)
  • Promotion has no integrity gate: raft_cb_become_leader (ha.c:1615) computes safe_lsn from votes (ha.c:1641-1644) then persist_truncate_wal_above(safe_lsn) (ha.c:1662) with no check that the local log is intact or ≥ safe_lsn. (Note: this describes the pre-spec baseline; citation corrected from the original ha.c:572/577. The gate this spec adds is now implemented immediately after, at ha.c:1699-1822.)
  • Freshness floor is volatile: ha_vote_self_freshness = max(applied_lsn, last_known_committed_lsn) (now ha.c:5310, corrected from the original ha.c:2127), in-memory atomics not re-derived from durable WAL.
  • Test-seam convention: #ifdef XCE_TESTING hook shims are now spread across dozens of sites in ha.c (the file has roughly doubled since this spec closed); wal_sync_ms was a hard constant (config.h:86, still DEFAULT_WAL_SYNC_MS = 10) with no override — this spec added the --wal-sync-ms override (confirmed live in main.c/persist.h). (Note: the original ha.c:2270-2335 range no longer corresponds to a single representative hook-shim cluster.)

Architecture Pattern & Boundary Map

graph TB
    subgraph RequestPath
        Hook[AFTER_EVENT hook off iomgr]
        Barrier[persist_commit_barrier]
    end
    subgraph Persistence
        Append[persist_wal_async sync fsync]
        DurLsn[durable_lsn]
        Recover[persist_recover integrity verdict]
        ReplApply[persist_wal_write_replicated standby fsync]
    end
    subgraph Commit
        Majority[majority_candidate_locked durable self]
        Committed[committed_lsn]
    end
    subgraph Election
        Fresh[freshness floor from durable WAL]
        Promote[raft_cb_become_leader promotion fence]
    end
    Hook --> Append
    Append --> DurLsn
    Append --> ReplApply
    DurLsn --> Majority
    ReplApply --> Majority
    Majority --> Committed
    Committed --> Barrier
    Barrier --> Reply[reply ok to client]
    Recover --> Fresh
    Recover --> Promote
    Fresh --> Promote
    DurLsn --> Promote

Architecture Integration

  • Selected pattern: extend-in-place for the durability precondition (Req 1, 3) plus a small testable fence helper for promotion eligibility (Req 2). No new module — durable_lsn is one atomic on persist_t.
  • Boundaries: persistence owns durable_lsn and the recovery verdict; the commit engine consumes durable_lsn; election consumes the recovery verdict + durable-backed floor. No shared ownership of the commit index.
  • Patterns preserved: commit-barrier reply gate, in_catch_up fence concept, XCE_TESTING hooks, the standby persist-before-ACK already in place.
  • Steering compliance: never block the iomgr thread (fsync lands on the off-iomgr commit path); re-verify against raft/raft.tla (commit rule, leader completeness) per CLAUDE.md.

Technology Stack

Layer Choice / Version Role in Feature Notes
Backend / Services C (gnu17), controller daemon Durable commit, recovery integrity, promotion fence Extends persist.c, commit.c, ha.c, cluster.c
Data / Storage Local WAL segments + fdatasync Synchronous durability; integrity-verified recovery posix_fallocate'd segments; fdatasync (data + pre-allocated metadata)
Infrastructure / Runtime --wal-sync-ms (new) + XCE_TESTING seam Deterministic durability verification Follows --sync-timeout-ms (OPT_SYNC_TIMEOUT) precedent

File Structure Plan

Modified Files

  • src/controller/persist.c — persist_wal_async: append then signal the flusher (no inline per-entry fsync); convert fsync_worker from a timer wait into a demand-driven group-commit flusher (wake on append-signal, fdatasync, advance durable_lsn to the highest synced LSN, broadcast the commit-eval condvar); keep its thread/mutex/cond lifecycle in persist_start/persist_stop/persist_fini. replay_wal/persist_recover: return an integrity verdict; re-derive durable floor from the recovered WAL tip. persist_wal_sync_append: resolved (task 2.4) — re-routed rather than deleted. It now calls the guarded sync_append_legacy_commit_store (persist.c:5617), which only advances committed_lsn when written_lsn <= durable_lsn (regression-pinned by test_legacy_sync_append_holds_committed_at_durable). (Note: current state corrected — as of this audit persist_wal_sync_append (persist.c:5639) DOES have a live production caller, submit_job_wal_entry_and_commit (persist.c:5990-6004, wired by raft-apply-decoupling), contradicting this section's original "dormant, no production caller" framing; the durable-precondition guard was added as designed, so the resolution is correct even though the "dormant" premise no longer holds.)
  • src/include/persist.h — add _Atomic uint64_t durable_lsn and a recovery-verdict type to persist_t/the recover signature; keep fsync_* fields (now driving the group-commit flusher); add an override field to persist_config_t (or its setter). Confirmed current: durable_lsn at persist.h:275, RECOVER_CLEAN/RECOVER_TRUNCATED enum, recover_decision_t, recovery_unrecoverable flag all present as designed.
  • src/controller/commit.c — majority_candidate_locked: use durable_lsn (not highest_appended_lsn) for the self contribution cap. Confirmed current (commit.c:135, persist_durable_lsn(ce->p)).
  • src/controller/ha.c — raft_cb_become_leader: insert the pre-promotion eligibility gate; ha_vote_self_freshness: derive floor from durable WAL state; fence-release on catch-up completion. (Note: the durability-verification XCE_TESTING seam actually lives in src/controller/persist.c — persist_test_set_force_fsync_fail at persist.c:1547, persist_test_durable_lsn_on_disk at persist.c:1610 — not in ha.c as this section originally stated.)
  • src/controller/cluster.c — vote / PreVote freshness comparison consume the durable-backed floor; promotion path honors the fence. (Note: citations corrected — real-vote comparison now at cluster.c:544-557, PreVote at cluster.c:643-651; original cited cluster.c:380-396/467-474.)
  • src/include/config.h — keep DEFAULT_WAL_SYNC_MS; reconcile the stale 50 in persistence-and-ha-design.md.
  • src/controller/main.c — parse --wal-sync-ms (and optionally --wal-sync-disable) into persist_config_t.
  • src/controller/myapp.c / cluster.c (persist_config_defaults callers) — apply the override before persist_init.

New Files

  • src/controller/testsuite/test_commit_durability.c — unit/white-box tests for durable_lsn advancement, self-counts-durable, recovery verdict, promotion fence (Req 1, 2, 3).
  • src/tools/test-commit-durability.sh — exists (soak E2E); extend to drive the new --wal-sync-* seam for a deterministic mode.

Each modified function keeps one responsibility: persistence owns durability + recovery verdict; commit owns majority math (consuming durable_lsn); election owns eligibility (consuming the verdict + floor).

System Flows

Durable commit (reply ok ⇒ persisted on a majority)

sequenceDiagram
    participant Client
    participant Primary
    participant Standby
    participant Flusher
    Client->>Primary: submit op
    Primary->>Primary: persist_wal_async pwrite then signal flusher
    Primary->>Standby: replicate entry
    Flusher->>Flusher: batched fdatasync then durable_lsn advance then wake commit
    Standby->>Standby: persist_wal_write_replicated fdatasync
    Standby-->>Primary: WalAck acked_lsn
    Primary->>Primary: majority_candidate_locked self equals durable_lsn plus standby acks
    Primary->>Primary: committed_lsn advance then commit barrier releases
    Primary-->>Client: reply ok

Key decisions: the reply is released only after committed_lsn covers the entry, and committed_lsn now requires a durable self plus a durable standby majority. The fdatasync runs on the dedicated flusher thread (the repurposed fsync_worker), batched across all pending appends; the AFTER_EVENT caller blocks on the commit barrier (off iomgr) until durable_lsn + standby acks cover its entry, so heartbeats are unaffected (Req 1.6) and one fdatasync amortizes across the high-volume RETAIN-fact stream.

Recovery integrity & promotion fence

graph TD
    Start[startup persist_recover] --> Replay[replay_wal]
    Replay --> Verdict{integrity verdict}
    Verdict -->|clean eof| Floor[set durable floor from WAL tip]
    Verdict -->|corruption truncated| Truncated[mark recovery_truncated]
    Floor --> Eligible[eligible to lead]
    Truncated --> CanCatchUp{healthy peer reachable}
    CanCatchUp -->|yes| Fence[fence from promotion until caught up]
    CanCatchUp -->|no| LoudFence[LOUD PERMANENT FENCE: non-promotable, STAYS ALIVE, keeps retrying catch-up — NEVER self-exit]
    LoudFence --> Caught
    Fence --> Caught{caught up past last committed boundary}
    Caught -->|yes| Eligible

Key decisions: corruption is never silently accepted (Req 2.1). A truncated member is fenced from promotion and catches up from a healthy primary (Req 2.2, 2.6); if it cannot reach a consistent committed state, the controller logs a LOUD operator-visible alert and holds itself PERMANENTLY non-promotable while STAYING ALIVE and continuing to retry catch-up (Req 2.4) — it refuses to serve divergent state by refusing leadership, NOT by terminating. A controller MUST NEVER self-exit (exit/abort) as a designed response to an operational condition (user invariant, 2026-06-18): a self-exited controller needs manual admin recovery and degrades quorum meanwhile, whereas one that stays alive self-heals when a peer returns (Req 2.6). A candidate never advertises or leads beyond its durable WAL tip (Req 2.3), so a hollow node cannot win even under degraded quorum (Req 2.5).

Requirements Traceability

Requirement Summary Components Interfaces Flows
1.1 reply ok ⇒ durable on majority DurableCommit commit barrier, durable_lsn Durable commit
1.2 self counts only when durable DurableCommit majority_candidate_locked Durable commit
1.3 standby persists before ACK DurableCommit (pin) persist_wal_write_replicated Durable commit
1.4 no premature ok DurableCommit persist_commit_barrier Durable commit
1.5 survives minority crash+restart DurableCommit durable-majority property Durable commit / soak
1.6 durability work preserves liveness DurableCommit off-iomgr placement Durable commit
2.1 no silent truncate-accept RecoveryIntegrity replay_wal verdict Recovery fence
2.2 fence until caught up PromotionFence promotion gate, in_catch_up Recovery fence
2.3 never lead below high-water PromotionFence + FreshnessFloor raft_cb_become_leader, ha_vote_self_freshness Recovery fence
2.4 loud permanent non-promotable fence when unrecoverable (stays alive, NEVER self-exit) RecoveryIntegrity loud-fence policy + sticky recovery_unrecoverable flag Recovery fence
2.5 degraded quorum preserves invariant DurableCommit + PromotionFence durable-majority + fence Both
2.6 re-eligibility on catch-up PromotionFence fence-release hook Recovery fence
3.1 configurable durability cadence DurabilityConfig --wal-sync-ms —
3.2 recoverable after ungraceful kill in verify mode DurabilityTestSeam XCE_TESTING hook soak deterministic mode
3.3 identical external semantics in/out of mode DurabilityTestSeam seam affects timing only —

Components and Interfaces

Component Layer Intent Req Coverage Key Dependencies (P0/P1) Contracts
DurableCommit Persistence + Commit Synchronous persist + self-counts-durable 1.1–1.6, 2.5 persist_t (P0), commit_engine (P0), repl ACK (P1) State
RecoveryIntegrity Persistence Verdict on recovery; durable floor; loud permanent non-promotable fence policy (stays alive, NEVER self-exit) 2.1, 2.4 replay_wal (P0) State
PromotionFence Election Eligibility gate + fence-release 2.2, 2.3, 2.6, 2.5 RecoveryIntegrity (P0), in_catch_up (P1) State
FreshnessFloor Election Durable-backed vote floor & advertisement 2.3 durable_lsn (P0), ha_state (P1) State
DurabilityConfig + TestSeam Runtime / Test Override cadence; verification hook 3.1–3.3 persist_config (P0), XCE_TESTING (P1) State

Persistence + Commit

DurableCommit

Field Detail
Intent Make the primary persist before it contributes to the commit majority
Requirements 1.1, 1.2, 1.3, 1.4, 1.5, 1.6, 2.5
  • persist_wal_async appends and signals the flusher; it does not fsync inline per entry.
  • The group-commit flusher (repurposed fsync_worker) wakes on the append-signal, performs one fdatasync, advances durable_lsn to the highest synced LSN, and broadcasts the commit-eval condvar — amortizing one sync across all entries pending at wake time (the high-volume RETAIN stream benefits most).
  • majority_candidate_locked caps the self contribution at durable_lsn, not highest_appended_lsn.
  • Standby persist-before-ACK is preserved and regression-pinned (persist_wal_write_replicated, defined at persist.c:1193, fdatasync call at persist.c:1417; note corrected from the original persist.c:515); the standby path may later adopt the same flusher (out of scope here).
  • Checkpoint markers retain their existing inline fdatasync (persist.c:1761; note corrected from the original persist.c:573, which now falls inside unrelated term-index code added by ha-term-safety).
  • durable_lsn is monotonic, never exceeds the live segment tip; on persist_truncate_wal_above, clamp durable_lsn to the new tip.

Dependencies

  • Inbound: AFTER_EVENT hooks (job.c, queue.c, worker.c, join.c), ha.c WAL_NOOP — purpose: append path (P0).
  • Outbound: commit_engine_t — purpose: self contribution input (P0).

Contracts: State [x]

State Management
  • State model: _Atomic uint64_t durable_lsn on persist_t; invariant durable_lsn <= current_lsn - 1, monotonic non-decreasing except clamp-on-truncate.
  • Persistence & consistency: durable_lsn advances only after a successful fdatasync in the flusher; the commit engine reads it for self-coverage so committed_lsn ⇒ durable-majority.
  • Concurrency strategy: the flusher takes p->lock to read the appended tip and fdatasync, advances durable_lsn, releases, then signals commit-eval; majority_candidate_locked reads durable_lsn via atomic load. Define the append-signal → flush → commit-wake ordering precisely so a WAIT caller cannot miss a wake (lost-wakeup guard).

Implementation Notes

  • Integration: the WAIT-mode caller blocks on the commit barrier off the iomgr thread; only the flusher thread blocks on fdatasync. Heartbeats unaffected.
  • Validation: assert committed_lsn <= durable_lsn on the local member after every commit advance (debug build); verify the flusher batches (one fsync advances durable_lsn past multiple LSNs under load).
  • Risks: lost-wakeup / batching-window correctness between persist_wal_async signal and the flusher (an entry must never be considered durable before its fdatasync); design the signal as level-triggered on the appended-vs-synced gap, not edge-triggered. Bounded flush latency vs throughput is a tunable (--wal-sync-ms becomes the max batching delay, not a durability gap).

Persistence — RecoveryIntegrity

Field Detail
Intent Distinguish clean log end from corruption; re-derive durable floor; loud permanent non-promotable fence when unrecoverable (stays alive, NEVER self-exit)
Requirements 2.1, 2.4

Responsibilities & Constraints

  • replay_wal/persist_recover return a verdict: RECOVER_CLEAN (reached a clean entry boundary) vs RECOVER_TRUNCATED (stopped at CRC break / mismatch / short read).
  • On RECOVER_TRUNCATED, the member is marked recovery-truncated and is NOT treated as a clean recovery; it must not advertise or lead beyond the last intact LSN.
  • The recovered durable floor (highest intact replayed LSN) is published so the freshness advertisement is durable-backed.
  • Loud-fence policy (NEVER self-exit, user invariant 2026-06-18): if a recovery-truncated / behind member cannot reach a healthy peer to catch up, the controller logs a LOUD operator-visible alert (truncation boundary vs cluster HWM) via persist_recover_loud_fence_if_unrecoverable, sets a sticky recovery_unrecoverable flag, and holds itself PERMANENTLY non-promotable while STAYING ALIVE and continuing to retry catch-up. It refuses to serve divergent state by refusing leadership — it does NOT exit/abort. The flag clears (and the fence releases → eligible, Req 2.6) automatically when a peer returns and catch-up reaches a committed-consistent state.

Contracts: State [x]

State Management
  • State model: verdict enum + recovery_truncated flag (on ha_state_t or persist_t); recovered durable floor = highest intact LSN.
  • Persistence & consistency: does not persist committed_lsn; only re-derives the durable log tip from on-disk segments.
  • Concurrency strategy: runs single-threaded during cluster_init_phase2 before the node participates.

Implementation Notes

  • Integration: composes with ha-convergence-recovery — that spec truncates an intact log on demotion/rejoin; this spec refuses to accept a corrupt log silently.
  • Validation: unit test injects a CRC break at LSN 1 and asserts verdict RECOVER_TRUNCATED + non-promotability.
  • Risks: must not loud-fence on a legitimately empty first-boot WAL (no entries ≠ corruption).

Boot Policy Decision Table (task 3.2)

Status: DECISION recorded (task 3.2); terminal action corrected by the never-self-exit rework (2026-06-18). The original table's FATAL outcome (a self-abort) was REPLACED: the unrecoverable terminal is now a LOUD PERMANENT FENCE — non-promotable, stays alive, keeps retrying catch-up. This table is the contract that task 3.3 (the loud-fence terminal) and task 4.3 (the promotion fence + release) implement.

Decision (Req 2.2, 2.4): A member that boots with a structurally clean log but below the cluster's committed high-water mark, or with a recovery-truncated log, is fenced from leadership at boot (never promoted while behind/truncated). It then attempts catch-up from a healthy peer. It becomes eligible only once catch-up brings its durable position to a committed-consistent state at/above the cluster boundary. If it cannot reach that state (no healthy peer reachable / cannot reach a committed-consistent state), it enters a LOUD PERMANENT FENCE: it logs a loud, operator-visible alert (truncation boundary vs cluster HWM), holds itself permanently non-promotable, and stays alive while continuing to retry catch-up — it NEVER self-terminates. The fence releases (→ ELIGIBLE) automatically once catch-up reaches a committed-consistent state.

Invariant (authoritative): A truncated/behind member always resolves to exactly one of two outcomes: it catches up → ELIGIBLE, or it enters a LOUD PERMANENT FENCE (non-promotable, stays alive, keeps retrying catch-up — NEVER self-exit). It is never silently divergent (it refuses to lead), and the process never self-exits/aborts as a designed response to this operational condition (user invariant, 2026-06-18) — a self-exited controller needs manual admin recovery and degrades quorum, whereas one that stays alive self-heals when a peer returns (Req 2.6). Snapshot-sentinel recovery is treated as CLEAN-but-behind (catch-up), never the unrecoverable terminal on a legitimate sentinel.

Inputs (evaluated at boot / promotion-eligibility):

  • verdict — recovery integrity verdict from task 3.1: CLEAN vs TRUNCATED.
  • durable-vs-HWM — local durable position relative to the cluster committed high-water mark: at/above vs below.
  • peer — a healthy peer reachable for catch-up: yes vs no.
  • catch-up — catch-up reaches a committed-consistent state within the bounded window: succeeds vs fails (n/a when no catch-up is attempted).

Outcomes:

  • ELIGIBLE — may promote (no fence).
  • FENCE+CATCH-UP → ELIGIBLE — ineligible to promote; catch up from a healthy peer; regain eligibility on success (Req 2.6).
  • LOUD PERMANENT FENCE — log a loud operator-visible alert (truncation/boundary), set the sticky recovery_unrecoverable flag, and hold the member permanently non-promotable while it stays alive and keeps retrying catch-up — NEVER self-exit; releases → ELIGIBLE on catch-up (Req 2.4, 2.6).
# verdict durable-vs-HWM healthy peer catch-up result Outcome Rationale / Req
1 CLEAN at/above n/a n/a ELIGIBLE Log intact and not behind — normal promotable member. (Req 2.3)
2 CLEAN below yes succeeds FENCE+CATCH-UP → ELIGIBLE Intact but behind the HWM; must not lead below the boundary; catch up then promote. (Req 2.2, 2.3, 2.6)
3 TRUNCATED (below — a truncated log is by definition not provably at/above) yes succeeds FENCE+CATCH-UP → ELIGIBLE Structurally truncated but a healthy peer exists; fence, catch up, regain eligibility. Never the unrecoverable terminal when a peer is reachable. (Req 2.2, 2.6)
4 TRUNCATED below no fails (no committed-consistent state reachable) LOUD PERMANENT FENCE (non-promotable, stays alive, keeps retrying catch-up — NEVER self-exit) Cannot recover locally AND no peer to catch up from ⇒ log loudly + hold non-promotable + alive; releases → ELIGIBLE when a peer returns and it catches up. NEVER exit/abort. (Req 2.4, 2.6)
4b CLEAN below no fails (no peer to advance from) LOUD PERMANENT FENCE (non-promotable, stays alive, keeps retrying catch-up — NEVER self-exit) Behind the HWM and no healthy peer to catch up from — same non-terminating loud-fence as row 4; NEVER self-exit. (Req 2.4, 2.2, 2.6)
5 CLEAN (snapshot-sentinel: committed at sentinel LSN, no sub-sentinel entries) below (no entries below the sentinel) yes succeeds FENCE+CATCH-UP → ELIGIBLE A legitimate sentinel snapshot is CLEAN-but-behind, NOT corruption; treat as must-catch-up, never the unrecoverable terminal on a legitimate sentinel. (Req 2.1, 2.2)
6 CLEAN at/above (empty first-boot WAL, fresh cold start: durable=0, HWM=0) n/a n/a ELIGIBLE An empty first-boot WAL is not behind anything — cold-start members are promotable. (Req 2.1, 2.3)

Notes on the dimensions:

  • A TRUNCATED verdict is never simultaneously "provably at/above the HWM": truncation means the log stops below its last intact boundary, so a truncated member is treated as behind for fence purposes regardless of the volatile in-memory position (this is why 4.2/3.4 derive the freshness floor from the durable WAL tip, not a volatile value).
  • the catch-up retry is indefinite (the member stays alive and keeps trying) and loud (a periodic operator-visible re-alert, controlled by DEFAULT_RECOVERY_CATCHUP_WINDOW_MS); it is never silently divergent because the member refuses leadership the entire time. The previous "bounded window before FATAL" deadline was REMOVED by the never-self-exit rework — there is no deadline-driven termination.
  • The healthy peer = no + at/above combination does not need catch-up and is covered by row 1 (ELIGIBLE) — a member already at/above the HWM is promotable without a peer.

Election — PromotionFence + FreshnessFloor

Field Detail
Intent Bar a truncated/behind member from leadership until caught up; advertise/vote on durable WAL state
Requirements 2.2, 2.3, 2.5, 2.6

Responsibilities & Constraints

  • Pre-promotion gate in raft_cb_become_leader: if recovery-truncated, or local durable position < cluster committed high-water mark, refuse promotion (set/extend in_catch_up-style fence) and instead catch up from a healthy primary.
  • ha_vote_self_freshness: floor derives from the durable WAL tip (re-derived on recovery), so a truncated member cannot over-advertise a volatile last_known_committed_lsn. Honors CLAUDE.md: the post-election safe-commit point still comes from voter replies, never from a stale ctrlhello.
  • Fence-release: when catch-up brings the member past its last-known committed boundary, restore eligibility (hook the existing catch-up completion / re-inclusion path).
  • Degraded quorum: because a candidate cannot lead beyond its durable tip, a hollow node cannot win even at minimal quorum — preserving Req 1's invariant across leadership changes.

Contracts: State [x]

Implementation Notes

  • Integration: reuses in_catch_up (ha.c:917, cluster.c:713; note corrected from the original ha.c:954/cluster.c:529) and the PreVote/vote freshness comparison (cluster.c:544-557 real-vote, cluster.c:643-651 PreVote; note corrected from the original cluster.c:380-396/467-474); extends the fence from "streaming standby" to "recovery-truncated / behind-high-water promoter."
  • Validation: simulate a node restarting truncated; assert it is denied promotion until catch-up, then re-enabled (Req 2.2/2.6).
  • Risks: interaction with ha-single-leader-role own-term gate and ha-prevote — re-verify the combined eligibility predicate against raft.tla.

Freshness-Floor Formula (task 4.1)

Status: PINNED (task 4.1, gating). This section is the authoritative contract that tasks 4.2 (implement the floor in ha.c/cluster.c) and 4.3 (promotion gate) implement against. Verification method: this is a manual conceptual-alignment + Protocol Verification Checklist argument, NOT a TLC run — there is no TLA+ toolchain in this environment (no tla2tools.jar/TLC/java). The argument maps the formula to raft/raft.tla's mlastLogIndex/LastTerm semantics and to the src/controller/CLAUDE.md checklist. Per the spec scope note, raft.tla validates the election/freshness logic this change touches; it does not validate the durability of the floor — that is verified by tests 3.4 / 2.x, because raft.tla assumes a durable log (see Non-Goals and §5.3 of the broader Raft model).

1. The pinned formula

Let, on member M:

  • durable_floor(M) = persist_durable_floor(M) — the durable WAL tip (task 3.4): the highest LSN whose bytes are fdatasync'd locally, re-derived on recovery as the highest intact replayed LSN (the truncation boundary on RECOVER_TRUNCATED, the clean tip on RECOVER_CLEAN). This is a durable last-log index, not the commit position.
  • learned_committed(M) = last_known_committed_lsn(M) — the volatile learned cluster commit high-water (a hint, possibly stale across a truncating restart).
  • learned_tag(M) = committed_config_tag(M), local_tag(M) = config_version_tag — the config epoch (compared first; unchanged by this task).

(a) What a candidate ADVERTISES (mlastLogIndex analog):

cand_lsn = durable_floor(M)            // NOT max(applied_lsn, learned_committed)
cand_tag = max(local_tag, learned_tag) // config epoch, unchanged

The candidate advertises exactly its durable WAL tip. It does not advertise applied_lsn (which can exceed the durable tip — entries applied to volatile state but not yet fdatasync'd) and does not advertise learned_committed (a hint that, after a truncating restart, can exceed the durable tip the node actually holds). This is the core change: a candidate may only claim a log position it can durably back. cand_tag is unchanged — config-epoch freshness is orthogonal to log durability.

(b) What a voter uses as its freshness FLOOR (the reconciliation):

voter_floor_lsn = max( durable_floor(M), learned_committed(M) )
voter_floor_tag = max( local_tag(M), learned_tag(M) )      // unchanged

The voter floor is the max of its own durable tip and its learned cluster-committed high-water. This is the precise reconciliation of the durable-derived floor against the existing max(applied_lsn, last_known_committed_lsn):

  • applied_lsn is replaced by durable_floor (a node must not demand of a candidate a position it itself only holds volatilely; and symmetrically must not under-advertise — see §3/§4). Note applied_lsn and durable_floor use different conventions and are not directly comparable as raw counters: applied_lsn is advanced to last_good_lsn — the last contiguously-held LSN — via ha_advance_applied_lsn (ha.c:3050, called at ha.c:3426-3432), whereas durable_floor/durable_lsn is the actual durable LSN watermark (the highest LSN whose bytes are fdatasync'd). (Note: this audit found the convention itself has since changed — the code comment at ha.c:3426-3429 cites a later fix, bug-991, that moved applied_lsn from last_good_lsn + 1 [the next-expected index this section originally described, cited at the now-stale ha.c:1234/1253] to bare last_good_lsn, "not last_good_lsn + 1," because the +1 wedged the leader's catch-up streamer. This does not affect the argument here — the two quantities were already established as not directly comparable, and the safety/liveness proof in §3/§4 does not rely on the exact applied_lsn convention.) We therefore do not rely on a raw durable_floor ≤ applied_lsn inequality. The claim that this term never raises the floor beyond what is reachable rests entirely on the D* argument in §4: the voter floor's local-state contribution durable_floor(v) is bounded above by D* (the most-durable reachable candidate's tip) by definition of D*, so swapping in durable_floor cannot push the floor above some reachable candidate ⇒ cannot newly induce livelock (§4).
  • learned_committed is retained as the safety backstop established by bug-339: a voter must never grant to a candidate below what the cluster has already committed, even if this voter's own durable tip is colder. Committed entries are now durable on a majority (Req 1/2.x), so at least a majority of voters carry that committed LSN in their durable_floor and every voter that learned the commit carries it in learned_committed — keeping the floor at the committed high-water on the voter side closes the window where a lagging voter would otherwise grant to a sub-committed candidate.

(c) The exact comparison (candidate ≥ voter floor — logOk analog):

grant_freshness(cand, voter) ==
       cand_tag >  voter_floor_tag
    \/ ( cand_tag == voter_floor_tag  /\  cand_lsn >= voter_floor_lsn )

i.e. deny iff cand_tag < voter_floor_tag, or cand_tag == voter_floor_tag && cand_lsn < voter_floor_lsn. Term-then-index ordering, matching raft's LastTerm-then-mlastLogIndex lexicographic order; here the config epoch (tag) is the high-order key (raft's LastTerm) and the durable LSN is the low-order key (raft's mlastLogIndex). Equality at both ⇒ grant (a node at least as fresh, including exactly as fresh, is grantable — preserves the existing >= semantics and idempotent re-grant).

Candidate and voter use DIFFERENT quantities — this is the load-bearing distinction, and the implementation must keep the two paths separate:

Citation note (this audit): the site line numbers below are corrected to their current locations; ha.c and cluster.c have grown substantially since this spec closed (2026-07-18) from later work (ha-term-safety, raft-apply-decoupling, job-array-single-wal-record, and unlisted in-flight specs). The mechanism itself is unchanged and verified current — a dedicated helper ha_candidate_advertise_lsn(persist_t *p) (ha.c:5347-5349, added since this spec's original text, which described inline snapshotting instead) now wraps the bare persist_durable_floor(p) call for both candidate sites.

Role Site(s) Quantity it must produce How
Candidate (advertised cand_lsn) ha.c:7938 (real-vote snapshot), ha.c:8017 (PreVote snapshot) — corrected from the original ha.c:3660-3666/3735-3741 bare durable_floor(M) — NOT folded with learned_committed calls ha_candidate_advertise_lsn(&c->persist) (ha.c:5347-5349), a thin wrapper over persist_durable_floor(p); do NOT route the advertised LSN through ha_vote_self_freshness
Voter (freshness floor voter_floor_lsn) cluster.c:544-557 (real-vote), cluster.c:643-651 (PreVote), ha.c:5436 (handle_request_vote, the XCE_TESTING-only legacy test gate) — corrected from the original cluster.c:388-395/471-475/ha.c:2243 max(durable_floor(M), learned_committed(M)) — the backstop is retained keep calling ha_vote_self_freshness, changing only its local_lsn input from applied_lsn to durable_floor(M); the function still folds in last_known_committed_lsn

Why the candidate must NOT reuse ha_vote_self_freshness. That function (ha.c:5310-5324; note corrected from the original ha.c:2127-2142) unconditionally computes *out_lsn = max(local_applied_lsn, last_known_committed_lsn). Feeding it durable_floor as the local input therefore yields max(durable_floor, learned_committed) — not the bare durable_floor §1a/§3 require. A truncated node with durable_floor = 4 but a stale volatile learned_committed = 8 would then advertise cand_lsn = 8 and win — exactly the truncated-candidate-wins hole this task closes (§5a). So 4.2 must give the candidate sites a candidate-only path that calls persist_durable_floor(p) directly and assigns it to cand_lsn, bypassing the learned_committed fold. (The candidate's cand_tag is still max(local_tag, learned_tag); only the LSN axis must bypass the fold.) The two PreVote/real-vote candidate snapshots currently call ha_vote_self_freshness for both fields — 4.2 splits the LSN field off onto the bare-durable_floor path while leaving the tag field on the existing max.

Why safety lives on the advertisement axis and the backstop lives on the voter axis. The candidate must not over-advertise beyond durable state — that is the safety requirement (§3): pinning cand_lsn = durable_floor is what denies a truncated candidate. The learned_committed backstop belongs on the voter axis (§3 dual guard): a voter must refuse any candidate below the cluster-committed boundary it learned, even when the voter's own durable tip momentarily lags. Folding learned_committed into the candidate advertisement would defeat the very safety property it protects on the voter side; folding it into the voter floor is exactly the bug-339 backstop. raft.tla confirms the split: RequestVote sends mlastLogIndex |-> Len(log[i]) — the bare candidate log length, with no committed term folded into the candidate's advertisement; the committed-high-water guard lives only on the voter's logOk floor. This recipe is now internally consistent with §1a (bare candidate durable_floor), §3 (quorum-intersection on the advertised durable_floor), and §4 (voter floor bounded by D*).

(d) safe_committed_lsn is UNCHANGED and still from voter replies. This floor governs only vote granting / advertisement. The post-election safe_committed_lsn is still computed by ha_compute_safe_committed_lsn (ha.c:1144; note corrected from the original ha.c:480/562) from the peerLastLogLsn values in the RequestVoteReply set, never from this floor and never from a stale ctrlhello (CLAUDE.md "Post-Election Safe Commit Point"). The reply's peer_last_log_lsn field (assigned at cluster.c:596 real-vote, cluster.c:735 PreVote; note corrected from the original cluster.c:426) now carries the durable-backed voter_floor_lsn, which is more conservative (never above a durable position), so the elected leader's safe_committed_lsn is if anything tightened, never loosened — persist_truncate_wal_above(safe_committed_lsn) still only removes entries strictly above a majority-backed point.

2. raft.tla alignment

raft.tla (HandleRequestVoteRequest, lines 284-289):

logOk == \/ m.mlastLogTerm > LastTerm(log[i])
         \/ /\ m.mlastLogTerm = LastTerm(log[i])
            /\ m.mlastLogIndex >= Len(log[i])

Mapping:

  • Len(log[i]) (voter's last-log index) ↔ voter_floor_lsn on the durable axis. Our durable WAL tip persist_durable_floor is the faithful analog of Len(log[i]): in raft.tla the log is restored intact from stable storage on restart (the model has no volatile-vs-durable distinction — every entry in log[i] is durable by assumption). By making committed entries durable on a majority (2.x) and deriving the advertised/floor index from persist_durable_floor (the on-disk tip) rather than a volatile applied_lsn, our cand_lsn/voter_floor_lsn become the genuine "length of the durable log," so the mlastLogIndex >= Len(log[i]) comparison holds with the same meaning the model assigns it.
  • m.mlastLogIndex (candidate's advertised index) ↔ cand_lsn = durable_floor(candidate) — exactly raft's mlastLogIndex |-> Len(log[i]) in RequestVote (line 196): the candidate advertises its own log length, which in our durable-log mapping is its durable tip. The pre-change code advertised max(applied_lsn, learned_committed), which could exceed Len(durable log) — an over-advertisement raft.tla cannot express (in the model you cannot advertise an index beyond Len(log[i])). The fix restores faithfulness to the model.
  • LastTerm(log[i]) / m.mlastLogTerm ↔ the config epoch tag. XCE folds per-entry Raft terms into a monotone config-version tag (single-writer log; term changes ride the config epoch); the high-order lexicographic key is preserved. This task does not change tag handling.

Caveat (restated): raft.tla does not model durability — it assumes log[i] survives restart intact, so it cannot itself prove that persist_durable_floor is durable. That property (the WAL-tip derivation is genuinely on stable storage and survives an ungraceful kill) is the subject of tests 3.4 and 2.x, not this alignment argument. What raft.tla does validate — and what this section argues we faithfully implement — is the election/freshness logic: with our durable tip standing in for Len(log), the logOk predicate and the Leader-Completeness proof carry over.

3. Leader Completeness (safety) — a truncated/behind candidate cannot win

Claim: under this formula, any candidate that wins an election holds all committed entries (raft's Leader Completeness).

Argument:

  1. By Req 1/2.x, an entry committed at LSN L is fdatasync'd on a majority Q_L of members; each member in Q_L has durable_floor ≥ L (durability is a contiguous prefix watermark — CLAUDE.md Commit Ordering — so a durable tip ≥ L implies all entries ≤ L are durable on that member).
  2. A candidate C needs votes from a majority Q_v. Any two majorities intersect: Q_L ∩ Q_v ≠ ∅, so at least one voter v has durable_floor(v) ≥ L, hence voter_floor_lsn(v) ≥ durable_floor(v) ≥ L.
  3. For v to grant, the comparison requires cand_lsn ≥ voter_floor_lsn(v) ≥ L. Since cand_lsn = durable_floor(C) (the candidate cannot advertise above its durable tip), durable_floor(C) ≥ L — C durably holds entry L (again by the prefix-watermark property, all entries ≤ L).
  4. Therefore a candidate whose durable tip is below the committed high-water L (a truncated or behind node) is denied by every voter in the intersection and cannot assemble a majority. The pre-change bug was that C could advertise learned_committed (or volatile applied_lsn) above its durable tip and thereby satisfy step 3 without durably holding L — winning, then truncating committed work away. Pinning cand_lsn = durable_floor(C) closes exactly that hole.

The retained learned_committed term in the voter floor (§1b) is the dual guard: even a voter whose own durable tip momentarily lags L (e.g. just rejoined) still refuses a candidate below the cluster-committed L it learned, so the safety margin does not depend on which majority voted.

4. Liveness (no election livelock) — the most-durable candidate can always win

Claim: the formula is not "too high" — among any available majority, the member holding the longest durable log can always be elected; the floor is always satisfiable by some reachable candidate, so there is no bug-339-style infinite election loop.

Argument:

  1. Let D* = max{ durable_floor(m) : m in an available majority A }, achieved by member C*. C* advertises cand_lsn = D*.
  2. The committed high-water L satisfies L ≤ D*: L is durable on a majority, that majority intersects A, so some member of A has durable_floor ≥ L, hence D* ≥ L.
  3. For any voter v ∈ A: voter_floor_lsn(v) = max(durable_floor(v), learned_committed(v)). We have durable_floor(v) ≤ D* by definition of D*. And learned_committed(v) ≤ L ≤ D* — a member never learns a committed LSN above the true committed high-water (learned_committed is a lower-or-equal estimate of L, advanced only from majority-acked commits / leader heartbeats). Therefore voter_floor_lsn(v) ≤ D* = cand_lsn(C*), so the comparison cand_lsn ≥ voter_floor_lsn(v) holds for every v ∈ A, and C* is grantable by the whole majority.
  4. Hence the floor is always satisfiable by the most-durable reachable candidate ⇒ an election can always complete ⇒ no livelock.

Why this avoids the bug-339 pattern specifically: bug-339 was an infinite loop because the RDHUP failover path advertised a stale committed_lsn that no longer matched the floor the (other) voters demanded — the advertiser claimed a position it could not satisfy against the floor, so it kept losing and retrying. Under the pinned formula no node advertises a position it cannot durably back (cand_lsn = durable_floor), and the voter floor is bounded above by D* (step 3, because both durable_floor(v) ≤ D* and learned_committed(v) ≤ L ≤ D*). The floor is therefore always met by C*. The earlier bug-339 fix pinned the voter floor to max(applied_lsn, last_known_committed_lsn); this task swaps the local-state term from the volatile applied_lsn to the durable durable_floor. Per §1b we do not rest on a raw durable_floor ≤ applied_lsn comparison (the two use different counter conventions); instead, the no-livelock guarantee rests solely on the D* bound of §4 — durable_floor(v) ≤ D* for every reachable voter v — so the swapped-in term can never push the voter floor above the most-durable reachable candidate C*. It therefore cannot reintroduce a too-high (livelock) floor while it closes the too-low (safety) hole on the advertisement side.

The safety/liveness tension is resolved, not papered over. The "too low ⇒ truncated node wins" failure lives on the advertisement axis (what a candidate may claim) and is fixed by cand_lsn = durable_floor (§3). The "too high ⇒ livelock" failure lives on the voter-floor axis (what a voter demands) and is avoided because the voter floor is bounded above by D*, the most-durable reachable candidate's tip (§4). The two fixes act on different sides of the same comparison, so there is no contradiction: §3 raises the floor for under-durable candidates without raising it beyond the best available candidate.

5. The two required cases

(a) Truncated-candidate DENIED. Node T restarts; its WAL hit a CRC break at LSN 5, so replay_wal returns RECOVER_TRUNCATED with durable_floor(T) = 4 (highest intact replayed LSN). Cluster committed high-water L = 8 (entries 5–8 are durable on the surviving majority Q). T becomes a candidate and advertises cand_lsn = durable_floor(T) = 4 (it cannot advertise the stale learned_committed = 8 it may still hold in volatile state — that is exactly the over-advertisement the formula forbids). Any voter v ∈ Q has durable_floor(v) ≥ 8, so voter_floor_lsn(v) ≥ 8 > 4 = cand_lsn ⇒ every such voter denies (§1c). T cannot reach a majority ⇒ not elected (Leader Completeness preserved, §3). Independently, the promotion fence (task 4.3) bars T from raft_cb_become_leader because persist_recovery_truncated(T) is true and durable_floor(T) < L — so even a degenerate quorum cannot promote it. T instead catches up from a healthy peer to durable_floor ≥ 8, then becomes both grantable and promotable (Req 2.6 / Boot Policy Decision Table row 3).

(b) Longest-durable-log STILL ELECTS (no livelock). Three nodes; the primary committed through LSN 8, so L = 8. Because committed ⇒ durable on a majority (Req 1/2.x), at least two of the three members hold durable_floor ≥ 8; the primary then died. The two survivors are A and B.

  • Sub-case L=8 is consistent with both survivors: the committing majority for L = 8 was some 2-of-3 set. If the dead primary was not in that majority, then both survivors A and B were in it ⇒ both have durable_floor ≥ 8. If the dead primary was in it, then exactly one of the two acking members survives; say A has durable_floor = 8 while B ended cleanly one entry behind at durable_floor = 7 (it appended/acked 8 against an earlier uncommitted round but its flusher had not advanced past 7 at crash — B is RECOVER_CLEAN, just behind, not truncated). Either way some survivor has durable_floor ≥ 8, so D* ≥ 8.

Take the tighter sub-case (A=8, B=7), where D* = 8 achieved by A. A advertises bare cand_lsn = durable_floor(A) = 8. Voter B: voter_floor_lsn(B) = max(durable_floor=7, learned_committed(B) ≤ L = 8). Here learned_committed(B) ≤ 8; if B had learned the L = 8 commit then voter_floor_lsn(B) = 8 = cand_lsn(A) ⇒ B grants (equality grants, §1c); if B only learned up to 7 then voter_floor_lsn(B) = 7 < 8 ⇒ B also grants. Either way B grants A, A self-grants ⇒ majority ⇒ A is elected (no livelock — consistent with §4 step 3, voter_floor_lsn(v) ≤ D*). Symmetrically B cannot win if A participates: B advertises bare cand_lsn = 7, and A's voter_floor_lsn = max(8, learned_committed_A ≤ 8) = 8 > 7 ⇒ A denies B, steering the election to the most-durable node A (§4).

The dangerous-looking livelock state is UNREACHABLE. The only way A could fail to be grantable by a majority is if some voter v had voter_floor_lsn(v) > cand_lsn(A) = D* — which by §4 step 3 requires learned_committed(v) > D*. But learned_committed(v) ≤ L (a node never learns a committed LSN above the true high-water) and L ≤ D* (committed ⇒ durable on a majority that intersects the survivors ⇒ some survivor has durable_floor ≥ L, so D* ≥ L). Hence learned_committed(v) ≤ L ≤ D* for every survivor v, so no survivor can demand a floor above D*, and a two-equal-tip-but-high-learned_committed deadlock (both survivors durable_floor = 5, both learned_committed = 8) cannot arise when L = 8 is genuinely committed: L = 8 committed forces some survivor to durable_floor ≥ 8 > 5, contradicting "both tips = 5". This is precisely the property §4 needs the case to demonstrate.

The elected A then computes safe_committed_lsn from the vote replies (durable-backed peer_last_log_lsn of A=8, B=7 ⇒ majority-backed safe point), unchanged by this task.

6. Protocol Verification Checklist pass (src/controller/CLAUDE.md)

Walking the relevant items under the pinned formula:

  • Freshness gate — candidate lastLogTerm >= voter AND lastLogIndex >= voter: HOLDS. The comparison (§1c) is cand_tag >= voter_floor_tag (term axis) AND, at equal tag, cand_lsn >= voter_floor_lsn (index axis) — exactly the checklist's two-key gate, now with lastLogIndex meaning the durable tip on both sides.
  • safe_committed_lsn derived from voter replies, not stale ctrlhello: HOLDS, UNCHANGED. This task does not touch ha_compute_safe_committed_lsn; it still reads votes[].peer_last_log_lsn (§1d). The floor change makes those replies durable-backed (more conservative), never sourced from a ctrlhello.
  • commitIndex / committed_lsn monotonic, contiguous prefix: HOLDS, UNCHANGED. The floor affects election only; commit advancement is untouched here (it is task 2.x). The freshness floor never writes committed_lsn.
  • WAL truncation on promotion only removes entries above the safe commit point: HOLDS. persist_truncate_wal_above(safe_committed_lsn) is unchanged; the durable-backed (tightened) safe_committed_lsn means truncation is, if anything, more conservative.
  • durable_lsn is a prefix watermark (never a per-entry set): HOLDS and is RELIED UPON — the Leader-Completeness argument (§3) and liveness argument (§4) both use "durable tip ≥ L ⇒ all entries ≤ L durable," which is exactly the prefix-watermark property the checklist asserts. cand_lsn/voter_floor_lsn are single LSNs (watermarks), not sets.
  • (post ha-commit-durability) a member counts toward the commit majority only at its durably-persisted LSN; acknowledged ⇒ durable on a majority: the election-side analog HOLDS here — a member contributes to a vote-grant (and advertises) only at its durably-persisted LSN. The commit-majority arithmetic side is task 2.x; this task makes the freshness/advertisement side durable-backed so the two are consistent.
  • votedFor updated atomically before granting; currentTerm monotonic: UNCHANGED by this task (term/vote bookkeeping in raft_on_vote_request is untouched); the floor change only gates whether grant is reached.

Concern / caveat (restated): raft.tla validates the freshness/election logic above; it does not validate that persist_durable_floor is genuinely durable (the model assumes a durable log). That durability is verified by tests 3.4 (durable-floor re-derivation on recovery) and 2.x (acknowledged ⇒ durable). No safety/liveness contradiction was found — the formula simultaneously satisfies Leader Completeness (§3) and no-livelock (§4) because the two pressures act on opposite sides of the comparison.

Runtime / Test — DurabilityConfig + TestSeam

Field Detail
Intent Deterministic, configurable durability timing for verification
Requirements 3.1, 3.2, 3.3

Responsibilities & Constraints

  • --wal-sync-ms plumbed main.c → persist_config_t before persist_init; default unchanged (DEFAULT_WAL_SYNC_MS). Under group-commit this bounds the maximum batching delay (a flush fires on the append-signal or when this elapses), never a durability gap — an acked op is always durable regardless of the value.
  • The seam's verification role: an XCE_TESTING hook (and/or a large --wal-sync-ms to widen the batching window) lets a test assert an acknowledged op is recoverable after an immediate ungraceful termination — proving durability comes from the commit gate, not the flush cadence.
  • External acknowledgment semantics are identical with or without the mode (timing controllability only).

Contracts: State [x]

Implementation Notes

  • Integration: follows --sync-timeout-ms (OPT_SYNC_TIMEOUT, main.c:32) convention; the actual durability test-seam functions live in src/controller/persist.c (persist_test_set_force_fsync_fail at persist.c:1547, persist_test_durable_lsn_on_disk at persist.c:1610), not at the originally-cited ha.c:2270-2335.
  • Validation: deterministic E2E mode in test-commit-durability.sh drives the seam so the soak becomes a deterministic RED on the unfixed build and GREEN after.
  • Risks: ensure the seam is compiled out of production (#ifdef XCE_TESTING).

Error Handling

Error Strategy

  • Durability failure (fdatasync error in the flusher): durable_lsn does not advance, so the entry is NOT counted durable, the commit does not advance, and the client does not receive ok (Req 1.4). The flusher surfaces the I/O error loudly (fail-loud); a persistent local sync failure is treated as a member fault, not silently retried into a false-durable state.
  • Recovery corruption (RECOVER_TRUNCATED): never silently accepted (Req 2.1). Fence from promotion + catch up; when catch-up is impossible (no peer) the node enters a LOUD PERMANENT FENCE — non-promotable, stays alive, keeps retrying catch-up, NEVER self-exits (Req 2.4, 2.6).
  • Promotion while behind: refused at the gate (Req 2.3); logged with the local durable tip vs the cluster high-water mark.

Monitoring

  • Log every durable_lsn regression-clamp on truncate, every recovery verdict (with the truncation boundary), every promotion refusal (durable tip vs high-water), and every fence set/release — operator-visible, once per transition (consistent with the quorum-transition logging already in the HA stack).

Testing Strategy

Unit Tests

  • durable_lsn advances only after fdatasync; majority_candidate_locked self-cap equals durable_lsn not highest_appended_lsn (1.2).
  • replay_wal returns RECOVER_TRUNCATED on an injected CRC break at LSN 1 and RECOVER_CLEAN on an intact log (2.1).
  • Promotion gate denies a recovery-truncated / behind-high-water member and re-enables it after catch-up (2.2, 2.6).
  • ha_vote_self_freshness floor reflects the durable WAL tip, not a stale in-memory last_known_committed_lsn (2.3).
  • Standby persist_wal_write_replicated fdatasyncs before ACK — regression pin (1.3).

Integration Tests

  • Commit advances committed_lsn only when self is durable + a standby ACK is durable; reply released only after (1.1, 1.4).
  • Kill the sole durable contributor mid-commit; acknowledged op survives on the majority (1.5).
  • Durability work does not delay heartbeat handling beyond tolerance (1.6).

E2E / Failover

  • src/tools/test-commit-durability.sh soak: rolling SIGKILL+restart under load asserts every acknowledged job survives (1.1, 1.5, 2.x). With the --wal-sync-* seam, run a deterministic variant: widen/disable background timing, kill a durable contributor in-window, assert survival — RED on the current build, GREEN after the fix (3.1, 3.2).

Performance

  • Measure submit latency delta from synchronous fdatasync vs the existing replication round-trip; confirm it is within the round-trip already paid before deciding group-commit is needed (research item).

Performance & Scalability

  • Group-commit amortizes one fdatasync across all entries pending at flush time, so the per-entry sync cost falls as load rises — critical for the high-volume WAL_MODE_RETAIN fact stream (job start/finish/fail/rusage) which is not client-latency-bound. --wal-sync-ms bounds the maximum batching delay (a latency/throughput tunable), never a durability gap. The job-array-single-wal-record roadmap item independently cuts per-array entry count. Target: zero acknowledged-job loss across failover (correctness) takes precedence over per-submit latency; group-commit keeps the throughput cost sub-linear in write rate.

Open Questions / Gating Items (resolve in /kiro-spec-tasks)

  • Freshness-floor formula (gating, election-safety): pin the exact reconciliation of the durable-WAL-derived floor vs the existing max(applied_lsn, last_known_committed_lsn). Too low ⇒ a truncated node still wins (the bug); too high ⇒ election livelock. Make a raft/raft.tla Leader-Completeness and liveness re-check a blocking sub-task before the freshness change merges (Req 2.3).
  • Unrecoverable-terminal decision point (gating): a booting truncated member cannot know it is "required for quorum" at cluster_init. Concrete policy: fence at boot, attempt catch-up from a healthy primary, and on a failure to reach a committed-consistent state (no peer) enter a LOUD PERMANENT FENCE — non-promotable, stays alive, keeps retrying catch-up, NEVER self-exit (Req 2.2, 2.4, 2.6). RESOLVED (task 3.2; terminal corrected by the never-self-exit rework 2026-06-18 — the original self-abort FATAL was replaced by the loud permanent fence): see the Boot Policy Decision Table (task 3.2) above; tasks 3.3 (loud-fence terminal) and 4.3 (fence + release) implement it.
  • Flusher lost-wakeup proof: the append-signal → flush → commit-wake path must be shown free of lost wakeups (level-triggered on the appended-vs-synced gap) before relying on it for the durability invariant (Req 1.1, 1.2).
  • Snapshot-recovery edge: current snapshots are 16-byte LSN sentinels (no entity data), so a member that recovers "from snapshot" has a committed position at the sentinel LSN but no log entries below it. The recovery verdict (3.1) must treat snapshot-sentinel + clean replay as CLEAN (not TRUNCATED), and the promotion fence (4.3) must treat such a member as behind-and-must-catch-up (never the unrecoverable terminal on a legitimate sentinel snapshot). Interacts with the roadmap entity-bearing snapshots item; pin the classification before implementing 3.1/4.3 (Req 2.1, 2.2).
  • Synchronous-append path — RESOLVED (task 2.4), re-verified current: persist_wal_sync_append (persist.c:5639) no longer advances the commit position unguarded — it routes through sync_append_legacy_commit_store (persist.c:5617), which only stores past committed_lsn when written_lsn <= durable_lsn, closing the ACK-without-durability hole (Req 1.1, 1.2; regression-pinned by test_legacy_sync_append_holds_committed_at_durable). (Note: this audit found the path is NOT dormant as originally described here — it now has a live production caller, submit_job_wal_entry_and_commit (persist.c:5990-6004), introduced by raft-apply-decoupling. The guard makes this safe regardless, so no further fix is needed, but the "no production caller today" premise in this section's original text no longer holds.)