Rongsong Shen
20e59d0b42
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.
210 lines
13 KiB
Markdown
210 lines
13 KiB
Markdown
# Implementation Plan
|
||
|
||
> **TDD-mandatory** (`testing.md`): every checker, scheduler action, and scenario lands as
|
||
> a RED test in `src/lib/testsuite/test_raft.c` (with the `raft_sim.c` backing) that fails
|
||
> before the harness logic exists and passes after. Build/run library tests via
|
||
> `/xce-build lib`. All harness code is `XCE_TESTING`-gated.
|
||
>
|
||
> **Spec boundary** (applies to ALL tasks): this spec owns `src/lib/raft/raft_sim.c`, the
|
||
> `XCE_TESTING` sim section of `src/lib/raft/raft.h`, and the conformance tests in
|
||
> `src/lib/testsuite/test_raft.c` ONLY. It does **NOT** modify the protocol
|
||
> implementation: no task changes `raft.c` protocol logic or any protocol declaration in
|
||
> `raft.h`, and no task edits a controller file. The harness drives the published library
|
||
> entry points and consumes the `raft-log-replication` + `raft-commit-safety` callback
|
||
> contract **verbatim**.
|
||
>
|
||
> **Depends** (whole spec): `raft-log-replication` (log model + AppendEntries entry points
|
||
> + the four callbacks), `raft-commit-safety` (`raft_advance_commit`, `on_commit_advanced`,
|
||
> `(lastLogTerm, lastLogIndex)` freshness). If those signatures change, re-validate per the
|
||
> design's Revalidation Triggers.
|
||
|
||
## 1. Harness types and in-memory adapter backing
|
||
|
||
- [ ] 1.1 Extend the `XCE_TESTING` sim section of `raft.h` with the harness data types
|
||
- Add `raft_sim_msg_kind_t`, `raft_sim_msg_t` (vote/AE req+rsp union fields), `raft_sim_log_entry_t {term, value}`, `raft_sim_action_t {kind, actor, msg_index, term, index}`, and the `RAFT_SIM_MAX_LOG/MSGS/STEPS` bounds
|
||
- Extend `raft_sim_node_t` with `log[]`, `log_len`, `commit_index`, `applied[]`, and a persisted-`(term, votedFor)` shadow for Restart; extend `raft_sim_cluster_t` with `bag[]`+`bag_count`, PRNG state, `seed`, and `trace[]`+`trace_len`
|
||
- Observable completion: `raft.h` compiles under `XCE_TESTING`; no protocol declaration changed; `sizeof(raft_sim_cluster_t)` grows by the new fixed arrays
|
||
- _Requirements: 1.1, 1.3, 2.5_
|
||
- _Boundary: raft.h (XCE_TESTING section only)_
|
||
|
||
- [ ] 1.2 Implement the seeded PRNG and the in-memory adapter callbacks
|
||
- Add a small inlined deterministic generator (e.g. SplitMix64) seeded by `cluster.seed`; add `on_persist_entry` → `node.log[]`, `on_get_entry_term` → term|0, `on_truncate_from` → shrink `log_len`, `on_commit_advanced` → set `commit_index` + apply into `applied[]`; route `on_send_vote_request`/`on_send_append_entries` to a bag push
|
||
- Add `raft_sim_conformance_init(c, n, timeout, seed)` wiring all six callbacks + the bag
|
||
- Observable completion: a test initializes a cluster, drives one `raft_log_append` on a forced leader, and reads the entry back via the in-memory log and `on_get_entry_term`
|
||
- _Requirements: 1.1, 1.2, 2.1_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 1.1_
|
||
|
||
## 2. Message bag (mirrors raft.tla `messages`)
|
||
|
||
- [ ] 2.1 RED+GREEN: bag push/deliver routes vote and AppendEntries RPCs through the library handlers
|
||
- Test: pushing a vote-req and an AE-req then delivering them invokes `raft_on_vote_request` / `raft_on_append_entries_request`, and the handler reply is pushed back as a `*_RSP` message
|
||
- Implement `raft_sim_bag_push` and `raft_sim_bag_deliver(i)` (route by `kind`, honor `node.partition`, push replies)
|
||
- Observable completion: delivered requests produce matching responses in the bag; partitioned endpoints are not delivered
|
||
- _Requirements: 2.2, 2.4_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 1.2_
|
||
|
||
- [ ] 2.2 RED+GREEN: Drop / Duplicate / Reorder mutate only the bag
|
||
- Test: `raft_sim_bag_drop`/`_duplicate` change bag multiplicity without mutating any node's term/role/log; reorder delivers in a PRNG-chosen order
|
||
- Implement the three bag operations (mirroring `raft.tla:443`/`448` `UNCHANGED` of non-message vars)
|
||
- Observable completion: node snapshots are identical before/after a drop or duplicate of an undelivered message
|
||
- _Requirements: 2.5_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 2.1_
|
||
|
||
## 3. The four invariant checkers (TDD against hand-built clusters)
|
||
|
||
- [ ] 3.1 RED+GREEN: Election Safety checker (P)
|
||
- Test: a cluster with two `LEADER` nodes at the same term fails; a single-leader-per-term cluster passes
|
||
- Implement `raft_sim_check_election_safety` over roles+terms read from `raft_snapshot`
|
||
- Observable completion: both directions assert correctly
|
||
- _Requirements: 3.1, 3.6_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 1.1_
|
||
|
||
- [ ] 3.2 RED+GREEN: Log Matching checker (P)
|
||
- Test: two logs sharing `(idx, term)` but differing earlier fail; identical-prefix logs pass
|
||
- Implement `raft_sim_check_log_matching` (pairwise; shared `(idx, term)` ⇒ identical `1..idx`)
|
||
- Observable completion: both directions assert correctly
|
||
- _Requirements: 3.2, 3.6_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 1.1_
|
||
|
||
- [ ] 3.3 RED+GREEN: Leader Completeness checker (P)
|
||
- Test: a committed `(index, term)` absent from a higher-term leader's log fails; present passes
|
||
- Implement `raft_sim_check_leader_completeness` using `commit_index` + per-node logs, tracking the highest-term leader to date
|
||
- Observable completion: both directions assert correctly
|
||
- _Requirements: 3.3, 3.6_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 1.1_
|
||
|
||
- [ ] 3.4 RED+GREEN: State Machine Safety checker (P)
|
||
- Test: divergent `applied[k]` across two nodes fails; identical applied prefixes pass
|
||
- Implement `raft_sim_check_state_machine_safety` over `applied[]`
|
||
- Observable completion: both directions assert correctly
|
||
- _Requirements: 3.4, 3.6_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 1.1_
|
||
|
||
- [ ] 3.5 RED+GREEN: `raft_sim_check_all` returns the first failing invariant and halts
|
||
- Test: a cluster violating two invariants reports the first; a clean cluster returns OK
|
||
- Implement `raft_sim_check_all` composing 3.1–3.4 in a fixed order
|
||
- Observable completion: first-failure semantics verified
|
||
- _Requirements: 3.5_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 3.1, 3.2, 3.3, 3.4_
|
||
|
||
## 4. Action scheduler and trace recorder
|
||
|
||
- [ ] 4.1 RED+GREEN: trace recorder records every action before it is applied
|
||
- Test: after a fixed step sequence, `cluster.trace[]` holds the actions in order; `raft_sim_dump_trace` prints seed, n, and the ordered actions
|
||
- Implement `raft_sim_action_t` recording (R1.4) + `raft_sim_dump_trace` (R5.1, R5.2); quiet on success unless `RAFT_SIM_VERBOSE` (R5.4)
|
||
- Observable completion: a recorded trace round-trips to a readable dump
|
||
- _Requirements: 1.4, 5.1, 5.2, 5.4_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 1.1_
|
||
|
||
- [ ] 4.2 RED+GREEN: `raft_sim_step` drives one Next-equivalent action through the library and checks invariants
|
||
- Test: stepping reaches each enabled action kind over a run; every step calls `raft_sim_check_all`; a forced violation halts with a trace dump and a `<0` return
|
||
- Implement the seeded scheduler dispatch (Restart, Timeout, RequestVote/BecomeLeader via vote delivery, ClientRequest, AppendEntries via `raft_send_append_entries`, AdvanceCommitIndex via `raft_advance_commit`, Receive via bag deliver, Duplicate/Drop) selecting only **enabled** actions, driving **only** library entry points
|
||
- Observable completion: a multi-step run touches log append, AE replication, commit advance, and message faults; invariants checked each step
|
||
- _Requirements: 2.1, 2.2, 2.3, 2.4, 2.6, 3.5_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 2.2, 3.5, 4.1_
|
||
|
||
- [ ] 4.3 RED+GREEN: Restart preserves persisted `term`/`votedFor`/log
|
||
- Test: a Restart action re-inits a node while keeping `node.log[]`, recovered `log_len`, and last-persisted `(term, votedFor)`; volatile state resets per `raft.tla` `Restart`
|
||
- Implement the Restart branch (feed `initial_log_len` + restored `(term, votedFor)` into `raft_init`)
|
||
- Observable completion: a restarted node retains its log and term; no invariant violation results from the restart alone
|
||
- _Requirements: 2.1_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 4.2_
|
||
|
||
- [ ] 4.4 RED+GREEN: deterministic replay from `(n, seed, max_steps)`
|
||
- Test: two runs with the same `(n, seed, max_steps)` reach identical final per-node + bag state and an identical recorded trace
|
||
- Implement `raft_sim_run(c, max_steps)` and confirm no wall-clock/address/uninitialized input leaks into choices
|
||
- Observable completion: byte-identical replay verified across two runs
|
||
- _Requirements: 1.5, 1.6, 5.3_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 4.2_
|
||
|
||
## 5. Targeted adversarial scenarios
|
||
|
||
- [ ] 5.1 Partition/heal scenario (P)
|
||
- Implement `raft_sim_scenario_partition_heal`: isolate a minority during appends, heal, drain the bag; assert all four invariants throughout and after convergence
|
||
- Observable completion: scenario passes with zero violations on the correct build
|
||
- _Requirements: 4.1_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 4.2_
|
||
|
||
- [ ] 5.2 Restart-churn scenario (P)
|
||
- Implement `raft_sim_scenario_restart_churn`: restart nodes mid-replication preserving persisted state; assert re-convergence with no violation
|
||
- Observable completion: scenario passes; restarted nodes converge to the leader's prefix
|
||
- _Requirements: 4.2_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 4.3_
|
||
|
||
- [ ] 5.3 Drop/duplicate/reorder scenario (P)
|
||
- Implement `raft_sim_scenario_drop_dup_reorder`: perturb bag delivery order + multiplicity; assert idempotent convergence with all four invariants held
|
||
- Observable completion: scenario passes; duplicated AE is a no-op (already-have branch)
|
||
- _Requirements: 4.3_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 4.2_
|
||
|
||
- [ ] 5.4 Figure-8 scenario
|
||
- Implement `raft_sim_scenario_figure8`: a previous-term entry on a quorum, a leader change; assert the entry is NOT reported committed until a current-term entry commits (Leader Completeness / State Machine Safety preserved)
|
||
- Observable completion: the previous-term entry's `commit_index` does not cover it until a current-term commit
|
||
- _Requirements: 4.4_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 4.2_
|
||
|
||
- [ ] 5.5 Stale-rejoin scenario (bug-851 G5)
|
||
- Implement `raft_sim_scenario_stale_rejoin`: a term-lagging node rejoins under a higher-term leader; assert it adopts the higher term from the AE/heartbeat path and does not re-elect at a reused term (Election Safety preserved)
|
||
- Observable completion: the rejoining node's term advances via AE; no duplicate-term leader appears
|
||
- _Requirements: 4.5_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 4.2_
|
||
|
||
## 6. CI batch and randomized seed sweep
|
||
|
||
- [ ] 6.1 RED+GREEN: randomized M-seed sweep with zero violations
|
||
- Test: run `raft_sim_run` for a fixed `max_steps` across M seeds (M ≥ configured minimum) plus all targeted scenarios; fail if any seed/scenario violates any invariant
|
||
- Implement the sweep harness in `test_raft.c`; bound `max_steps`, M, and array sizes so the target fits the library test-suite budget
|
||
- Observable completion: the full batch runs clean and within budget
|
||
- _Requirements: 6.1, 6.2, 6.4_
|
||
- _Boundary: test_raft.c_
|
||
- _Depends: 5.1, 5.2, 5.3, 5.4, 5.5_
|
||
|
||
- [ ] 6.2 Verify the conformance batch is ASAN/UBSAN-clean
|
||
- Run the conformance batch under the library test sanitizer build; fix any leak/overflow/UB in the harness (fixed-size arrays, no allocation)
|
||
- Observable completion: `/xce-build lib` sanitizer run reports no memory errors, leaks, or UB for the conformance target
|
||
- _Requirements: 6.3_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 6.1_
|
||
|
||
## 7. Deliberately-broken-build negative test (the oracle's teeth)
|
||
|
||
- [ ] 7.1 RED+GREEN: compile-time fault switch emulates the bug-851 defects in the adapter
|
||
- Implement `RAFT_SIM_BREAK_TERM_STAMP` (adapter `on_persist_entry` writes term 0) and `RAFT_SIM_BREAK_TRUNCATE` (adapter `on_truncate_from` no-op), confined to the test/harness build configuration; default off
|
||
- Observable completion: with a macro off, scenarios are clean; the macro is not set in the default CI run and does not touch `raft.c`
|
||
- _Requirements: 7.1, 7.3_
|
||
- _Boundary: raft_sim.c_
|
||
- _Depends: 5.4, 5.5_
|
||
|
||
- [ ] 7.2 RED+GREEN: negative test asserts both directions
|
||
- Test: under the broken configuration the Figure-8 / divergent-suffix scenario triggers a Log Matching / Leader Completeness / State Machine Safety violation (with trace dump); under the correct configuration the same scenario passes — both asserted in one test
|
||
- Observable completion: the broken build is caught and the correct build passes, proving checker sensitivity
|
||
- _Requirements: 7.1, 7.2, 7.4_
|
||
- _Boundary: test_raft.c_
|
||
- _Depends: 7.1_
|
||
|
||
## 8. Optional TLC-consumable trace export
|
||
|
||
- [ ]* 8.1 TLC-consumable trace export (deferred; off by default)
|
||
- Implement `raft_sim_export_trace` gated by `RAFT_SIM_EXPORT`: per step, emit the action + tracked `raft.tla` variables (`messages` summary, per-node `currentTerm`/`state`/`log`/`commitIndex`) named per `raft/raft.tla`, in a stable line-oriented format; off by default
|
||
- Observable completion: with `RAFT_SIM_EXPORT` set, a run emits a stable, spec-named record stream; default runs emit nothing extra
|
||
- _Requirements: 8.1, 8.2, 8.3_
|
||
- _Boundary: raft_sim.c, test_raft.c_
|
||
- _Depends: 4.2_
|
||
```
|