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

feat(raft-sim-conformance): Figure-8 commit-safety scenario + restore dropped 5.3 impl (task 5.4)

Browse source 
Adds raft_sim_scenario_figure8: a previous-term entry on a quorum under a
new-term leader is NOT committed until a current-term entry commits (library-
gated by raft_advance_commit; verified by a mutation test). Also restores the
raft_sim_scenario_drop_dup_reorder implementation that commit e445404 (task 5.3)
silently dropped from raft_sim.c (a stray git checkout reverted the uncommitted
impl), which had left the lib build broken with an undefined reference.

Build green: test_sim_5_3_drop_dup_reorder + test_sim_5_4_figure8 both PASS.
This commit is contained in:
Rongsong Shen 2026-06-24 15:38:01 +00:00
parent e445404439
commit b1f289d2cb
4 changed files with 521 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/lib/raft/raft.h
View file

@ -1037,6 +1037,36 @@ int raft_sim_scenario_restart_churn(raft_sim_cluster_t *c, int n, uint64_t seed)
*/
int raft_sim_scenario_drop_dup_reorder(raft_sim_cluster_t *c, int n, uint64_t seed);
/*
* raft_sim_scenario_figure8: canonical Raft Figure-8 commit-safety scenario
* (raft-sim-conformance task 5.4; Req 4.4). Initializes the caller's cluster from
* (n, election_timeout=2000, seed), then:
* 1. elects leader L1 at term T1 and physically replicates a PREVIOUS-term entry
* E1 to a QUORUM of logs (real raft_log_append + raft_send_append_entries +
* delivery) WITHOUT advancing commit over it,
* 2. forces a LEADER CHANGE to L2 at a strictly-higher term T2 (partition L1 away;
* a survivor campaigns and wins — being up-to-date, L2 necessarily HOLDS E1),
* 3. ASSERTS THE SAFETY PROPERTY: with E1 (a term-T1 entry) on a quorum under the
* term-T2 leader, raft_advance_commit must NOT cover E1 by replica count alone
* (the current-term Figure-8 rule, raft.c G4) — L2.commit_index stays below
* E1's index and NO node reports E1 committed,
* 4. L2 then appends a CURRENT-term entry E2, replicates it to a quorum, and
* raft_advance_commit now advances commit_index to cover BOTH E2 and
* (transitively) E1.
* raft_sim_check_all is run after EVERY action — so Leader Completeness and State
* Machine Safety are asserted THROUGHOUT, never only at the end (Req 4.1). The
* library enforces the commit rule; the harness only DRIVES raft_advance_commit and
* OBSERVES commit_index (it never re-implements the rule or forges commit_index).
* Returns 0 if the scenario completes with ZERO invariant violations AND the safety
* property holds (E1 uncommitted under T2 until the current-term commit, then
* committed transitively); < 0 (the negated first failing invariant, matching
* raft_sim_step) on any violation or if the property is broken, after dumping the
* replayable trace to stderr. Returns -1 on an invalid node count (n < 3). Drives
* only via published library entry points + harness primitives — no protocol
* re-implementation.
*/
int raft_sim_scenario_figure8(raft_sim_cluster_t *c, int n, uint64_t seed);
#endif /* XCE_TESTING */
#endif /* RAFT_H */