wdgzyjx/myxce
1
0
Fork 0
forked from lei.chen/myxce
Code Pull requests Activity

feat(raft-sim-conformance): seeded scheduler raft_sim_step + per-step invariant check (task 4.2)

Browse source 
Harness surfaced a real upstream raft.c split-brain bug (bug-1095/1096,
bug-851 family) in raft_on_vote_reply: counter-based vote tally double-counts
a duplicated vote-response and no stale-term drop -> two leaders same term.
Out of this spec's boundary (raft.c protocol); recorded as Implementation Note.
This commit is contained in:
Rongsong Shen 2026-06-24 13:37:03 +00:00
parent 90e7e9c999
commit e15bbf8190
4 changed files with 377 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -105,7 +105,7 @@
- _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
- [x] 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
@ -208,3 +208,22 @@
- _Boundary: raft_sim.c, test_raft.c_
- _Depends: 4.2_
```
## Implementation Notes
- **Task 4.2 — UPSTREAM raft.c BUG SURFACED (bug-1095/1096, bug-851 family).** While building
the scheduler, the conformance oracle detected a real split-brain defect in `raft.c`
`raft_on_vote_reply`: (1) vote grants are tallied with a plain counter that ignores
`from_idx`, so a legitimate `DuplicateMessage` of a vote-response double-counts toward
quorum; (2) there is no stale-term (`mterm < currentTerm`) reply drop. In `raft.tla`
`votesGranted` is a SET (idempotent under the legal Duplicate action) and
`DropStaleResponse` discards stale replies — so a correct implementation must tolerate
both. Result: two leaders at the same term (Election Safety violation) on some seeds.
This is OUT OF THIS SPEC'S BOUNDARY (raft.c protocol logic, owned by raft-core /
ha-term-safety). The harness must NOT mask it (R2.6). **Consequence for downstream
tasks:** any task asserting "zero invariant violations on the correct build" (5.x targeted
scenarios, 6.1 M-seed sweep, 7.2 correct-direction) may surface this defect. Implementers
of those tasks MUST NOT weaken the oracle or hand-pick seeds to hide the bug; if a
legitimate scenario surfaces it, report BLOCKED with the upstream cause rather than
working around it. Seed 3 is clean over 600 steps and is used only to prove the 4.2
scheduler mechanism reaches all action kinds.