feat(raft-sim-conformance): restart-churn adversarial scenario (task 5.2)

This commit is contained in:
Rongsong Shen 2026-06-24 14:47:25 +00:00
parent 7d0964dd16
commit 6976392d77
4 changed files with 304 additions and 1 deletions

View file

@ -138,7 +138,7 @@
- _Boundary: raft_sim.c, test_raft.c_
- _Depends: 4.2_
- [ ] 5.2 Restart-churn scenario (P)
- [x] 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_
@ -249,3 +249,17 @@
`min(commit_index)` when followers are at 0 (it silently passes). 5.1 was accepted as-is
(meets R4.1 via throughout-checking + log matching); 5.2–5.5 should propagate commit so
their commit assertions are non-vacuous.
- **CORRECTION (task 5.2, confirmed): this library uses a LEADER-ONLY commit model.**
`raft_on_append_entries_request` does `(void)leader_commit;` (raft.c:646-655) — a FOLLOWER
never advances its `commit_index`/`applied[]` from AppendEntries; `on_commit_advanced`
fires ONLY on the leader via `raft_advance_commit` (raft.c:816). This is intended XCE
design (follower commit visibility is a controller/heartbeat concern — see
ha-heartbeat-committed-propagation — not the raft library). CONSEQUENCE for scenarios: a
follow-up AE round does NOT advance follower commit; do NOT assert follower
`commit_index == leader commit_index`. Assert re-convergence over the LOG instead
(every node's `log_count` reaches the leader's tip + per-entry term match / Log Matching),
and assert leader-side commit via `leader.commit_index`. For 5.4 (Figure-8), the property
under test is LEADER-side (the leader must not mark a previous-term entry committed until a
current-term entry commits) — driven by `raft_advance_commit` on the leader, which works.
applied[]/SM-Safety is exercised across leader CHANGES (each node accumulates applied[]
while it is leader). This SUPERSEDES the follower-commit-propagation guidance above.