lei.chen/myxce
1
0
Fork 1
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

checkpoint: bug-851 root cause + raft TLA+ conformance spec family

Browse source 
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.
This commit is contained in:
Rongsong Shen 2026-06-21 14:02:15 +00:00
parent 7d70820aac
commit 20e59d0b42
85 changed files with 10525 additions and 1993 deletions
Download patch file Download diff file Expand all files Collapse all files

210
.kiro/specs/raft-sim-conformance/tasks.md Normal file
View file

@ -0,0 +1,210 @@
# 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_
```