myxce/.kiro/specs/raft-commit-safety/requirements.md
Rongsong Shen 20e59d0b42 checkpoint: bug-851 root cause + raft TLA+ conformance spec family
Investigation & fixes (failover committed-job loss):
- root-cause bug-851 on an owned 3-node cluster: chaotic failover causes
  silent committed-prefix divergence (WAL hdr.term always 0; two leaders
  per term; no (term,lsn) reconcile). Evidence in repro-851/ + INVESTIGATION.
- live-validated fixes 848/849/850 (recovery-on-promotion, advertise real
  applied_lsn, persist-layer contiguity guard); add waldump WAL inspector.

Specs (strict raft.tla conformance — library owns the log):
- TLA-gap-analysis.md: impl vs raft/raft.tla, gaps G1-G6.
- raft-log-replication, raft-commit-safety, raft-sim-conformance: extend
  src/lib/raft to own log/commit/verification via callbacks (specs generated,
  cross-spec review passed).
- ha-term-safety: controller-side adapter + config marker (R1-R7); design done.
- config-upgrade-snapshot: R8 descoped here (deps entity-bearing-snapshots, bug-857).
- roadmap + buglog (851/854/857) + .wolf knowledge updated.
2026-06-21 14:02:15 +00:00

18 KiB
Raw Blame History

Requirements Document

Introduction

src/lib/raft/raft.{c,h} is the pure, callback-driven Raft library for XCE. The raft-library spec gave it the election half of raft/raft.tla (Ongaro's canonical Raft TLA⁺), and the upstream raft-log-replication spec gave it the log half: a library-owned log where every entry carries a uint64_t term (1-based index = WAL LSN), ClientRequest append (raft_log_append), AppendEntries emission/handling, per-peer next_index[] / match_index[], the on_get_entry_term / on_persist_entry / on_send_append_entries / on_truncate_from callbacks, and UpdateTerm on every RPC. That upstream spec deliberately carries leader_commit opaquely through on_send_append_entries and raft_on_append_entries_request without acting on it — it never advances a commit index.

This feature closes the remaining two raft.tla safety gaps from the gap analysis (.kiro/specs/ha-term-safety/TLA-gap-analysis.md):

  • G4 — term-blind commit advance. raft.tla AdvanceCommitIndex (line 259) advances commitIndex to Max(agreeIndexes) only if log[Max(agreeIndexes)].term == currentTerm — the Figure-8 safety rule: a leader must never mark a previous-term entry committed by replica-count alone; it commits the older entry only indirectly, once an entry from its own current term reaches a quorum. XCE's commit barrier + ha_compute_safe_committed_lsn advanced committed term-blind ("from 1 granted voter") because the WAL term was dead (G1); the own-term WAL_NOOP gate is only a partial mitigation. This spec adds raft_advance_commit(...) to the library, computing agreeIndexes from per-peer match_index[] and advancing commit_index only when the entry at the max agreed index is from the current term, with a new on_commit_advanced(ctx, commit_index) callback that triggers the existing synchronous commit barrier.

  • G6 — LSN-only vote freshness. raft.tla HandleRequestVoteRequest logOk (line 285) compares the candidate's (lastLogTerm, lastLogIndex) against the voter's lexicographically: grant only if the candidate's last log term is strictly greater, or the terms tie and the candidate's last log index is at least the voter's. XCE's on_vote_eligible gate uses config_tag ≥ plus an applied/durable-LSN floor only — it never compares lastLogTerm. With G6 a node whose log has a higher term but a lower index can be denied (correct) or, worse, a stale-term-but-higher-index candidate can be wrongly granted. This spec upgrades the freshness gate on both the binding vote path (raft_on_vote_request) and the PreVote eligibility path to carry and compare last_log_term alongside the existing last_log_index.

The library core stays pure / synchronous / deterministic (no I/O, no threads, no allocation in the hot path): raft_advance_commit reads entry terms only through the existing on_get_entry_term callback and reports the new commit index only through on_commit_advanced; the controller adapter performs the durable commit work. The feature is verified end-to-end in the deterministic simulator (raft_sim.c) against Leader Completeness and the Figure-8 scenario, without a live cluster.

Boundary Context

  • In scope:

    • raft_advance_commit(...): compute agreeIndexes from the library's per-peer match_index[] (a quorum agrees, including self), and advance commit_index to Max(agreeIndexes) only when on_get_entry_term(Max(agreeIndexes)) == currentTerm (the Figure-8 current-term rule, raft.tla AdvanceCommitIndex line 259, closes G4). Otherwise hold commit_index unchanged.
    • A new commit_index field in the library state and the new required callback void on_commit_advanced(void *ctx, uint64_t commit_index) fired after commit_index strictly advances, so the controller adapter feeds it into the existing synchronous commit barrier / persist-before-ACK durability (the callback triggers commit-evaluation; it does not perform or replace the barrier).
    • (lastLogTerm, lastLogIndex) vote freshness (raft.tla HandleRequestVoteRequest logOk line 285, closes G6): carry last_log_term alongside last_log_index into the binding vote path (raft_on_vote_request) and the PreVote eligibility path, and grant only on the lexicographic (lastLogTerm, lastLogIndex) comparison.
    • Simulator coverage in raft_sim.c: a Figure-8 scenario (a previous-term entry replicated to a quorum but not yet committed by the current leader) asserting the library refuses to commit it until a current-term entry is committed; and a Leader Completeness assertion (a committed entry is present in every future leader's log) across forced leader changes.
  • Out of scope (owned elsewhere):

    • The library log model + ClientRequest / AppendEntries / HandleAppendEntries* / UpdateTerm-on-any-RPC, the per-entry term, and the per-peer next_index[] / match_index[] themselves → raft-log-replication (consumed here verbatim; not redefined).
    • The synchronous commit-barrier mechanism, fsync/group-commit, persist-before-ACK durability, the reply gate, and snapshot transport → controller (ha-term-safety adapter). This spec only triggers the barrier via on_commit_advanced; it neither implements nor weakens it.
    • Configuration-change markers in the unified log and the upgrade snapshot → ha-term-safety.
    • The full conformance / TLC trace-check harness → raft-sim-conformance.
    • The replacement of ha_compute_safe_committed_lsn's term-blind advance in the controller with the library's current-term-gated commit_index → that controller wiring is ha-term-safety; this spec defines only the library entry point and callback the controller will route through.
  • Adjacent expectations:

    • Builds on raft-log-replication (HARD dependency): needs the (term, index) library log, on_get_entry_term, and per-peer match_index[]. All of that contract is reused verbatim and not redefined here.
    • Preserves as policy (must NOT be canonicalized away): the synchronous commit barrier + persist-before-ACK durability are stronger than canonical Raft's async apply and remain — on_commit_advanced triggers the existing barrier, it does not replace it. PreVote and priority leadership are unchanged in mechanism; only the freshness predicate they consult gains last_log_term.
    • "Controller never self-terminates": the library returns status codes only; it never aborts a process. The controller owns liveness/fencing.
    • Feeds raft-sim-conformance (Leader Completeness oracle) and ha-term-safety (the controller integration that routes the WAL/commit barrier through raft_advance_commit + on_commit_advanced). Closes bug-851 G4/G6.

Requirements

Requirement 1: Library-owned commit index with the current-term advance rule (closes G4)

Objective: As the leader of a Raft cluster, I want my commit index to advance only over an index that a quorum holds and whose entry is from my current term, so that a previous-term entry is never marked committed by replica-count alone (Figure-8 safety) and Leader Completeness holds.

Acceptance Criteria

  1. The Raft Library shall maintain, per node, a commit_index (the raft.tla commitIndex) initialized to the value restored from the adapter at boot (default 0), so the library — not term-blind controller code — owns the commit position.
  2. When raft_advance_commit(...) is called while the node's role is RAFT_LEADER, the Raft Library shall compute agreeIndexes as the set of indexes index in 1..log_len for which the set {self} ∪ {peer : match_index[peer] ≥ index} is a quorum, mirroring raft.tla AdvanceCommitIndex agreeIndexes.
  3. When agreeIndexes is non-empty and on_get_entry_term(Max(agreeIndexes)) == currentTerm, the Raft Library shall set commit_index to Max(agreeIndexes), mirroring the raft.tla AdvanceCommitIndex newCommitIndex then-branch (the Figure-8 current-term rule).
  4. If agreeIndexes is empty, or on_get_entry_term(Max(agreeIndexes)) != currentTerm, then the Raft Library shall leave commit_index unchanged, mirroring the raft.tla AdvanceCommitIndex else-branch (refusing to commit a previous-term entry by replica-count alone).
  5. The Raft Library shall never decrease commit_index; raft_advance_commit shall be monotonic, only ever moving commit_index forward.
  6. If raft_advance_commit(...) is called while the node's role is not RAFT_LEADER, then the Raft Library shall leave commit_index unchanged and report a non-success status, mirroring the raft.tla AdvanceCommitIndex state[i] = Leader precondition.
  7. The Raft Library shall obtain the term of the entry at Max(agreeIndexes) exclusively through the existing on_get_entry_term callback and shall perform no storage I/O itself.

Requirement 2: on_commit_advanced callback triggering the existing commit barrier

Objective: As the XCE controller adapter, I want the library to notify me exactly when the committed position moves forward, so that I can drive the existing synchronous commit barrier / persist-before-ACK durability off the library's safe commit index without the library performing or weakening that durability work.

Acceptance Criteria

  1. The Raft Library shall define the required callback void on_commit_advanced(void *ctx, uint64_t commit_index), fired with the new commit_index after it strictly advances.
  2. When raft_advance_commit(...) advances commit_index to a strictly greater value, the Raft Library shall invoke on_commit_advanced(ctx, commit_index) exactly once with the new value.
  3. If raft_advance_commit(...) does not change commit_index (held by the current-term rule, empty agreeIndexes, or non-leader), then the Raft Library shall not invoke on_commit_advanced.
  4. The Raft Library shall treat on_commit_advanced as a trigger only: it shall not itself fsync, persist entries, send the client ACK, or otherwise implement the commit barrier — those remain the controller adapter's responsibility (persist-before-ACK durability preserved as policy).
  5. The Raft Library shall validate on_commit_advanced as a required, non-NULL callback at raft_init, returning -EINVAL when it is NULL, consistent with how existing required callbacks are validated.
  6. The Raft Library shall not advance commit_index or fire on_commit_advanced as a side effect of raft_on_append_entries_reply; updating per-peer match_index[] and advancing the commit index remain separate steps (mirroring raft.tla, where AdvanceCommitIndex is a distinct action from HandleAppendEntriesResponse).

Requirement 3: (lastLogTerm, lastLogIndex) vote freshness on the binding vote path (closes G6)

Objective: As any cluster member receiving a RequestVote, I want to grant my vote only to a candidate whose log is at least as up-to-date as mine by the (lastLogTerm, lastLogIndex) comparison, so that an election can never elect a leader missing a committed entry (Leader Completeness).

Acceptance Criteria

  1. When raft_on_vote_request(...) evaluates freshness, the Raft Library shall compute logOk = (cand_last_log_term > local_last_log_term) ∨ (cand_last_log_term == local_last_log_term ∧ cand_last_log_index ≥ local_last_log_index), mirroring the raft.tla HandleRequestVoteRequest logOk predicate (closes G6).
  2. The Raft Library shall accept the candidate's last_log_term alongside the existing last_log_index on the vote-request path so the (lastLogTerm, lastLogIndex) comparison can be made (extending the eligibility signature or the vote-request payload accordingly).
  3. The Raft Library shall obtain the voter's own local_last_log_term and local_last_log_index from its library log model (on_get_entry_term(log_len) and log_len, with term 0 when the log is empty), consistent with raft.tla LastTerm(log).
  4. If logOk is false, then the Raft Library shall deny the vote, even when all other Raft invariants (correct term, no prior vote this term) and application gates would otherwise grant it.
  5. The Raft Library shall apply the (lastLogTerm, lastLogIndex) freshness check without weakening the existing election-safety invariants (stale-term deny, one-vote-per-term, persist-before-grant) or the existing application policy gate (primary-deny / heartbeat stickiness / catch-up), which remain in force.
  6. The Raft Library shall preserve the existing persist-before-grant ordering: a vote that passes the (lastLogTerm, lastLogIndex) freshness check is persisted via on_persist before being granted.

Requirement 4: (lastLogTerm, lastLogIndex) freshness on the PreVote eligibility path (closes G6 for PreVote)

Objective: As a node answering a PreVote straw poll, I want to apply the same (lastLogTerm, lastLogIndex) freshness rule as the binding vote, so that PreVote never green-lights a candidacy that a real election would reject for log staleness — without mutating any persistent state.

Acceptance Criteria

  1. When raft_on_pre_vote_request(...) evaluates eligibility, the Raft Library shall apply the same (lastLogTerm, lastLogIndex) freshness predicate as the binding vote path (Requirement 3.1), using the candidate's advertised last_log_term and last_log_index.
  2. The Raft Library shall carry last_log_term alongside last_log_index on the PreVote eligibility path consistently with the binding vote path, so the two paths apply an identical freshness rule.
  3. If the (lastLogTerm, lastLogIndex) freshness predicate is false, then the Raft Library shall deny the PreVote.
  4. While answering a PreVote, the Raft Library shall not mutate currentTerm, voted_for, voted_for_term, role, or commit_index, and shall not invoke on_persist — preserving the existing PreVote side-effect-free invariant.
  5. The Raft Library shall keep the existing PreVote stale-term deny and application eligibility gate (on_vote_eligible) in force; the (lastLogTerm, lastLogIndex) freshness is applied in addition to them, not in place of them.

Requirement 5: Preserve the synchronous commit barrier and durability as policy

Objective: As the operator of an XCE HA cluster, I want the commit-safety upgrade to keep XCE's stronger-than-canonical durability guarantees intact, so that acknowledged work remains durable on a majority and the term-safety fix does not regress availability or durability behavior.

Acceptance Criteria

  1. The Raft Library shall expose the safe commit index only as a trigger (on_commit_advanced); the synchronous commit barrier, persist-before-ACK durability, fsync/group-commit, and the reply gate shall remain the controller adapter's responsibility and shall not be moved into or weakened by the library.
  2. The Raft Library shall not change the existing PreVote mechanism or priority-leadership behavior; the freshness predicate these paths consult gains last_log_term, and the locus of that freshness decision moves from the caller/dispatcher into the library (see Requirement 5.4).
  3. The Raft Library shall return status codes only and shall never abort a process on any commit-safety or freshness condition, preserving the "controller never self-terminates" invariant.
  4. The Raft Library shall leave all existing election and log-replication entry points and callbacks (from raft-library and raft-log-replication) behaviorally unchanged, except for: (a) the additive freshness arguments on the vote/PreVote paths, (b) the additive commit_index / on_commit_advanced state and callback, and (c) the freshness-decision locus move — the vote/PreVote entry points gain the last_log_term / last_log_index arguments and the library now owns the logOk decision that was previously the caller's/dispatcher's (the binding path no longer delegates freshness to on_vote_eligible, and the PreVote path no longer relies on the dispatcher applying freshness before the call).

Requirement 6: Deterministic Figure-8 and Leader Completeness verification in the simulator

Objective: As a maintainer, I want the deterministic simulator to drive commit advance and forced leader changes and assert the Figure-8 refusal and Leader Completeness, so that the commit-safety and freshness rules are verifiable without a live cluster.

Acceptance Criteria

  1. The Raft Simulator shall drive raft_advance_commit on the leader after replication so the commit index advances deterministically over the in-memory per-node log backing the existing callbacks.
  2. The Raft Simulator shall construct a Figure-8 scenario — a previous-term entry replicated to a quorum but not yet covered by a committed current-term entry — and shall assert that the library does not advance commit_index over that previous-term entry until an entry from the current term is committed.
  3. When the current-term entry that covers the previous-term entry is replicated to a quorum and raft_advance_commit is driven, the Raft Simulator shall assert that commit_index then advances over both entries (indirect commit of the previous-term entry).
  4. The Raft Simulator shall assert the Leader Completeness invariant across forced leader changes: any entry that was committed (present at or below commit_index on the committing leader) is present in the log of every node that subsequently becomes leader.
  5. The Raft Simulator shall exercise the (lastLogTerm, lastLogIndex) freshness gate: a candidate with a stale last-log-term shall be denied the vote even when its last-log-index is greater, and a candidate with a fresher last-log-term shall be granted regardless of a smaller last-log-index, asserting the lexicographic comparison.
  6. The Raft Simulator shall assert that on_commit_advanced fires exactly when commit_index strictly advances and does not fire when the current-term rule holds the commit index, so the trigger semantics consumed by the controller barrier are verified.