From 52ae598dfe50dd4d937c8979f48ea8eadc77909a Mon Sep 17 00:00:00 2001 From: Rongsong Shen Date: Thu, 30 Jul 2026 03:39:56 +0000 Subject: [PATCH] docs(raft-adapter-conformance): extend controller conformance record with this feature's findings CLAUDE.md's TLA+ Action-to-Code Mapping table gains corrected/new rows: production vs. dormant AppendEntries send mechanisms, WAL catch-up and config-push reply integrity, and vote/PreVote failure routing across all failure timings -- each citation independently re-verified against live source. The old AppendEntries row's citations had already drifted onto unrelated code before this task; corrected, not just appended to. Protocol Verification Checklist gains 3 new items for the guarantees this feature closes. ha-term-safety/spec.json's known_limitations entry for the dormant send-path drift gets an additive RESOLVED pointer back to this spec's disposition, so a future reader lands on the answer instead of re-discovering the drift. Requirement 1 (systematic conformance audit deliverable) complete. --- .kiro/specs/ha-term-safety/spec.json | 2 +- .kiro/specs/raft-adapter-conformance/tasks.md | 2 +- src/controller/CLAUDE.md | 11 ++++++++++- 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/.kiro/specs/ha-term-safety/spec.json b/.kiro/specs/ha-term-safety/spec.json index 224e43e..4e806aa 100644 --- a/.kiro/specs/ha-term-safety/spec.json +++ b/.kiro/specs/ha-term-safety/spec.json @@ -27,7 +27,7 @@ "note": "First post-implementation validation run -- all 19 tasks (1.1-5.5) were already [x] with no prior validate_impl record. Full suite 9/9 green, 46/46 requirement acceptance criteria mapped, fresh 6-round live chaotic-multi-kill soak PASS (zero committed divergence/job loss), boundary/dependency direction clean (src/lib/raft untouched across all 35 tagged commits).", "known_limitations": [ "design.md's 'Commit-source switch' section describes the originally-planned architecture (library commit_index replacing the term-blind safe-commit); as shipped (commit 83fbed2, reviewer-approved with a RED->GREEN Figure-8 safety proof), the durable-majority barrier + own-term WAL_NOOP gate remain authoritative and raft_commit_index is purely advisory (commit.c:154). Design doc not updated to match; behavior is correct and safety-proven, this is a documentation-drift note only.", - "design.md's AppendEntries send-side architecture (on_send_append_entries/raft_send_append_entries, task 2.3) is dormant in production per a later cross-spec comment (raft-ha-core-safety task 6.2, ha.c:2530-2536) -- the live send path is the pre-existing repl_broadcast, patched by task 3.4 to carry entry.term/prev_log_term. The receive side IS live and correctly processes these entries -- live-verified safe, just not what the design.md diagram depicts. Documentation-drift note only.", + "design.md's AppendEntries send-side architecture (on_send_append_entries/raft_send_append_entries, task 2.3) is dormant in production per a later cross-spec comment (raft-ha-core-safety task 6.2, ha.c:2530-2536) -- the live send path is the pre-existing repl_broadcast, patched by task 3.4 to carry entry.term/prev_log_term. The receive side IS live and correctly processes these entries -- live-verified safe, just not what the design.md diagram depicts. Documentation-drift note only. RESOLVED 2026-07-29: raft-adapter-conformance has now formally documented and regression-guarded this exact drift -- see src/controller/CLAUDE.md's TLA+ Action-to-Code Mapping table (the dormant nextIndex-driven sender row) and that spec's design.md 'Decision: dormant AppendEntries sender resolution' section for the authoritative disposition; a future reader should land there instead of re-discovering this drift.", "ha.c:1844 has a stale 'TODO(ha-term-safety task 2.x): REPLACE these stubs' header comment whose own body lines each say '-- IMPLEMENTED'; a companion stale doc-comment sits in ha_convergence.c ~357-360 describing retired behavior. Cosmetic only, self-flagged in tasks.md's own 5.5 cleanup list, never executed." ] } diff --git a/.kiro/specs/raft-adapter-conformance/tasks.md b/.kiro/specs/raft-adapter-conformance/tasks.md index b2b4928..47cce2b 100644 --- a/.kiro/specs/raft-adapter-conformance/tasks.md +++ b/.kiro/specs/raft-adapter-conformance/tasks.md @@ -76,7 +76,7 @@ - _Requirements: 5.3_ - _Boundary: test_commit_barrier_reply.c_ -- [ ] 6. Integration: extend the controller's durable conformance record with this feature's findings +- [x] 6. Integration: extend the controller's durable conformance record with this feature's findings - Update `src/controller/CLAUDE.md`'s "TLA+ Action-to-Code Mapping" table and "Protocol Verification Checklist" with corrected/added rows covering: `AppendEntries` reply integrity (WAL catch-up and configuration push), vote/PreVote failure routing across all failure timings, and the dormant-sender resolution from task 4 - Append a one-line pointer to the existing `known_limitations` entry (index 30) in `.kiro/specs/ha-term-safety/spec.json`, referencing this spec's resolution of the dormant `on_send_append_entries` send-path drift - Observable: the CLAUDE.md table cites the current, post-fix code paths for every action this feature touched, with no reference to the pre-fix silent-drop behavior as if it were still current; a reader of `ha-term-safety`'s known_limitations lands on this spec's resolution instead of re-discovering the drift diff --git a/src/controller/CLAUDE.md b/src/controller/CLAUDE.md index 38d2eba..9afa17f 100644 --- a/src/controller/CLAUDE.md +++ b/src/controller/CLAUDE.md @@ -62,10 +62,16 @@ The file `raft/raft.tla` contains Diego Ongaro's TLA+ specification of the Raft | `RequestVote(i,j)` | `raft_on_vote_request` / reply path | `raft.c:106,169` | | `BecomeLeader(i)` | `raft_cb_become_leader` | `ha.c:347` | | `AdvanceCommitIndex(i)` | `repl_wait_majority_ack` → advance `committed_lsn` | `repl.c:338` | -| `AppendEntries(i,j)` | `OPCode_nop` heartbeat + WAL streaming | `ha.c:2880`, `config_repl.c:1489` | +| `AppendEntries(i,j)` — production send (LIVE) | `repl_broadcast` (per-entry fan-out on append, NACK-driven retry via `ha_raft_on_repl_nack`) + `ha_stream_wal_to_standby` (catch-up-range streaming) — the sole production `AppendEntries`-equivalent send/retry/backoff mechanism (raft-adapter-conformance Req 3.3) | `repl.c:295`, `config_repl.c:2351` | +| `AppendEntries(i,j)` — nextIndex-driven sender (DORMANT, documented) | `raft_send_append_entries` is fully protocol-conformant but has ZERO production callers (only `raft_sim.c` and an `XCE_TESTING` test helper); its registered `on_send_append_entries` callback `ha_cb_send_append_entries_stub` is reachable only through it. Kept as an intentionally-dormant reference implementation (retire/wire-in both rejected, see `research.md`), guarded against silent regression by `ha_send_append_entries_stub_call_count` staying 0 while the production path fires (`test_ha_core_safety.c` task 4.2) | `src/lib/raft/raft.c:595`, `ha.c:2590` (stub), `ha.c:2588` (guard counter) | +| `AppendEntries(i,j)` reply — WAL catch-up reject | Every WAL catch-up rejection sends an explicit `WalAckReply{success=0}` via `ha_send_wal_ack_reply_ex` back to the primary — never a silent drop (bug-1479; reply-construction boundary regression-locked by raft-adapter-conformance task 5.1) | `ha.c:3155` (fn), `ha.c:3190` (accept call site), `ha.c:3326` (reject call site) | +| `AppendEntries(i,j)` reply — configuration-push accept/reject | Every `handle_repl_config_push` outcome — all 4 reject branches plus the success/`-EAGAIN`-activation-deferred tail — sends exactly one explicit `ReplConfigPushReply{accepted, term}` via `send_config_push_reply`, so the primary can distinguish an active reject from a lost push (raft-adapter-conformance Req 2.2-2.5); the reply's `term` field feeds the primary's `raft_on_higher_term_observed` term-adoption alongside the heartbeat and WAL-NACK vectors (Req 7.4/7.5) | `config_repl.c:1267` (send fn), `config_repl.c:1308-1381` (handler), `cluster.c:750-780` (primary-side accept/reject branch + term-adoption) | +| `RequestVote`/`PreVote(i,j)` reply — endpoint-failure routing, all timings | A vote/PreVote endpoint failure is always counted through the production tally (`vote_reply_dispatch` / `pre_vote_reply_dispatch`), never the legacy `handle_request_vote_reply` path — true both at connect-time (bug-1423/1424, regression-locked) and post-connect, i.e. a failure after connect but before a reply arrives (raft-adapter-conformance Req 4.2/4.3, closing that one remaining failure-timing gap). `vote_ep_err_handler` (real-vote) and `pre_vote_ep_err_handler` (PreVote) are separate handlers sharing one `CTRL_PRIMARY`-cleanup helper | `ha.c:7667` (`vote_ep_err_handler`), `ha.c:7705` (`pre_vote_ep_err_handler`), `ha.c:7627` (shared cleanup helper), registered at `ha.c:692` / `ha.c:831` | | `ClientRequest(i,v)` | Job submit → WAL append → `repl_wait_majority_ack` | `persist.c`, `repl.c` | | `UpdateTerm(i,j,m)` | Term CAS in `handle_request_vote` / vote reply handler | `ha.c:1218-1230` | +> Full gap-analysis citations, options considered, and design rationale for the `raft-adapter-conformance` rows above (including the dormant-sender decision and the vote/PreVote handler-split decision): `.kiro/specs/raft-adapter-conformance/research.md` and `design.md`. This table stays the terse, current pointer; the evidentiary trail lives there. + ### Safety Invariants Verified **Election Safety** (≤1 leader per term): Enforced by `votedFor` — a server grants at most one vote per term (`raft_on_vote_request` line 145-151). A candidate needs majority votes; each server votes at most once per term. @@ -107,6 +113,9 @@ When modifying HA protocol code (election, replication, heartbeat), verify: - [ ] Durability flushing makes a contiguous prefix durable; `durable_lsn` is a prefix watermark (never a per-entry set) - [ ] Causal dependencies are appended in order (cause before effect, e.g. submit before start) - [x] (post `ha-commit-durability`, landed 2026-06-18) a member counts toward the commit majority only at its durably-persisted LSN; acknowledged ⇒ durable on a majority +- [x] (post `raft-adapter-conformance`, landed 2026-07-29) every reject of a replication-class message (WAL catch-up entry, configuration push) sends an explicit reply distinguishable from a lost message — never a silent drop (`ha_send_wal_ack_reply_ex(success=0)` for WAL catch-up, bug-1479; `send_config_push_reply(accepted=0)` for config-push, Req 2.2-2.5) +- [x] (post `raft-adapter-conformance`, landed 2026-07-29) every vote/PreVote endpoint failure — connect-time or post-connect (a failure after connect but before a reply) — is counted through the production tally (`vote_reply_dispatch`/`pre_vote_reply_dispatch`), never the legacy `handle_request_vote_reply` path (Req 4.1-4.4) +- [x] (post `raft-adapter-conformance`, landed 2026-07-29) `raft_send_append_entries`/`ha_cb_send_append_entries_stub` remains dormant in production (zero callers) by deliberate documented decision, not oversight — `ha_send_append_entries_stub_call_count` stays 0 while `repl_broadcast`/`ha_stream_wal_to_standby` fire for the same scenario (Req 3.3) ## HA Design Constraints