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.
26 lines
2.7 KiB
Markdown
26 lines
2.7 KiB
Markdown
# Brief: raft-sim-conformance
|
|
|
|
## Problem
|
|
Once the library owns the full Raft protocol (election via `raft-library`, log via `raft-log-replication`, commit safety via `raft-commit-safety`), XCE needs an **independent verification harness** that proves the consensus core conforms to `raft/raft.tla` — without a live cluster, threads, or sockets. Today `raft_sim.c` exists but only exercises the election half; there is no oracle for the four Raft safety invariants. This is the "use the verified spec to help" payoff: a deterministic regression oracle that would have caught **bug-851** before it shipped.
|
|
|
|
## Approach
|
|
Extend `src/lib/raft/raft_sim.c` into a **conformance harness** that drives N library instances purely in-process through transitions equivalent to the `raft.tla` `Next` actions, and continuously checks the TLA+ safety invariants.
|
|
|
|
### TLA+ actions to drive (raft.tla `Next`, line 454)
|
|
`Restart`, `Timeout`, `RequestVote`, `BecomeLeader`, `ClientRequest`, `AppendEntries`, `AdvanceCommitIndex`, `Receive` (vote/AE request+response, `UpdateTerm`, drop-stale), `DuplicateMessage`, `DropMessage`. The harness owns a message bag and per-node state mirroring `raft.tla`'s variables.
|
|
|
|
### Invariants asserted every step (the four Raft safety properties)
|
|
1. **Election Safety** — at most one leader per term.
|
|
2. **Log Matching** — if two logs share an entry at `(index, term)`, all prior entries are identical.
|
|
3. **Leader Completeness** — an entry committed in term T is present in every leader's log for terms > T.
|
|
4. **State Machine Safety** — no two nodes apply different commands at the same index.
|
|
|
|
## Scope
|
|
- **In**: a deterministic, seedable driver (randomized + targeted scenarios: partitions, restarts, message drop/dup/reorder, Figure-8); per-step invariant checks; failure reproduction (print the action trace that broke an invariant); CI-runnable test target alongside the existing library tests. Optionally: emit a trace consumable by TLC, or compare against TLC-generated traces of `raft.tla`.
|
|
- **Out**: the protocol implementation itself (owned by the three upstream specs); the live controller / `/xce-deploy-ha` integration (that is `ha-term-safety`'s chaotic-failover regression); config markers/snapshot.
|
|
|
|
## Verification
|
|
The harness IS the verification. Acceptance: it reproduces a bug-851-class divergence on a deliberately-broken build (e.g. term stamping disabled, or `(term,lsn)` truncation removed) and passes on the correct build; it runs M randomized seeds in CI with zero invariant violations.
|
|
|
|
## Dependencies
|
|
`raft-log-replication`, `raft-commit-safety` (HARD — the harness checks invariants over the log + commit behaviour they add). Complements `ha-term-safety`'s live regression (this is the in-process oracle; that is the end-to-end one).
|