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

feat(raft-sim-conformance): State Machine Safety invariant checker (task 3.4)

Browse source
This commit is contained in:
Rongsong Shen 2026-06-24 12:51:58 +00:00
parent 63a9740c85
commit a38d9a7271
4 changed files with 119 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/lib/raft/raft_sim.c
View file

@ -882,6 +882,33 @@ int raft_sim_check_leader_completeness(const raft_sim_cluster_t *c)
return 1; /* holds */
}
int raft_sim_check_state_machine_safety(const raft_sim_cluster_t *c)
{
/* State Machine Safety: no two nodes have applied a different value at the same
* (1-based) log index. Observable-only (Req 3.6): each node's applied extent is
* 1..commit_index (on_commit_advanced fills applied[k-1] for committed index k).
* For every pair (a < b) and every index k in the shared applied prefix
* 1..min(commit_a, commit_b), fail if applied[k-1] differs. Pairs are symmetric,
* so a < b suffices. */
for (int a = 0; a < c->n; a++) {
const raft_sim_node_t *na = &c->nodes[a];
for (int b = a + 1; b < c->n; b++) {
const raft_sim_node_t *nb = &c->nodes[b];
uint64_t shared = na->commit_index < nb->commit_index
? na->commit_index : nb->commit_index;
if (shared > RAFT_SIM_MAX_LOG)
shared = RAFT_SIM_MAX_LOG;
for (uint64_t k = 1; k <= shared; k++) {
if (na->applied[k - 1] != nb->applied[k - 1])
return 0; /* divergent applied value — State Machine Safety violated */
}
}
}
return 1; /* holds */
}
int raft_sim_restart_node(raft_sim_cluster_t *c, int node_idx)
{
if (node_idx < 0 || node_idx >= c->n)