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

3.8 KiB

Raw Blame History

Brief: raft-commit-safety

Problem

After raft-log-replication gives the library a real (term, index) log, two raft.tla commit/election-safety rules are still missing in XCE (gap analysis: .kiro/specs/ha-term-safety/TLA-gap-analysis.md):

G4 — commit-index advance is term-blind. raft.tla AdvanceCommitIndex (line 259) only advances commitIndex to Max(agreeIndexes) if log[Max].term == currentTerm (the Figure-8 safety rule: a leader never commits a previous-term entry by replica-count alone). XCE's commit barrier + ha_compute_safe_committed_lsn advanced committed "from 1 granted voter" with no current-term check (because the WAL term was dead); the own-term WAL_NOOP gate is only a partial mitigation.
G6 — vote freshness is LSN-only. raft.tla HandleRequestVoteRequest logOk (line 285) compares (lastLogTerm, lastLogIndex) lexicographically; the library's on_vote_eligible gate uses config_tag ≥ + applied LSN ≥ only — it never compares lastLogTerm.

Approach

Add the commit-safety and freshness rules to the library, strictly per raft.tla, on top of the raft-log-replication log model.

TLA+ actions implemented

AdvanceCommitIndex(i) (raft.tla:259) → raft_advance_commit(...): compute agreeIndexes from per-peer matchIndex (a quorum agrees), and advance commitIndex to Max(agreeIndexes) only when on_get_entry_term(Max) == currentTerm. Otherwise hold.
HandleRequestVoteRequest logOk (raft.tla:285) → upgrade the freshness gate to (lastLogTerm, lastLogIndex): grant only if cand.lastLogTerm > local.lastLogTerm ∨ (== ∧ cand.lastLogIndex ≥ local.lastLogIndex), applied to both raft_on_vote_request and the PreVote eligibility path.

Authoritative shared contract

Uses the raft-log-replication contract verbatim (1-based index = WAL LSN; per-entry uint64_t term; on_get_entry_term, per-peer matchIndex). New callback:

void on_commit_advanced(void *ctx, uint64_t commit_index) — fired AFTER commitIndex advances; the controller adapter feeds this into the existing synchronous commit barrier / durability (persist-before-ACK preserved — this callback does not replace the barrier, it triggers commit-eval). Vote RPC freshness gains last_log_term alongside the existing last_log_index/config_tag carried to on_vote_eligible (extend the eligibility signature or the vote-request payload accordingly).

Scope

In: AdvanceCommitIndex with the current-term rule; (lastLogTerm, lastLogIndex) vote/PreVote freshness; on_commit_advanced callback wired to the controller commit barrier; simulator assertion of Leader Completeness (a committed entry is present in every future leader's log).
Out: the log model + AppendEntries (owned by raft-log-replication); the conformance harness (raft-sim-conformance); config markers/snapshot (ha-term-safety); the barrier/durability mechanism itself (controller — this spec only triggers it via on_commit_advanced).

Preserve as policy

The synchronous commit barrier + persist-before-ACK durability is STRONGER than canonical Raft async apply and MUST remain: on_commit_advanced triggers the existing barrier; it does not weaken it. PreVote and priority leadership unchanged.

Verification

Extend raft_sim.c: construct Figure-8 scenarios (a previous-term entry replicated to a quorum but not yet committed by the current leader) and assert the library refuses to commit it until a current-term entry is committed; assert Leader Completeness across forced leader changes. Replace ha_compute_safe_committed_lsn's term-blind advance with the library's current-term-gated commitIndex.

Dependencies

raft-log-replication (HARD — needs the (term,index) log + matchIndex). Feeds raft-sim-conformance and ha-term-safety. Closes bug-851 G4/G6.

3.8 KiB Raw Blame History Unescape Escape