lei.chen/myxce
1
0
Fork 1
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

docs(raft-sim-conformance): cosmetic cleanups (LOW review nits)

Browse source 
- sim_tla_action_name: drop brittle per-case 'raft.tla:NNN' line-number comments
  (some had drifted a few lines off; the return string IS the stable raft.tla
  Next-disjunct name, and the function header already cites raft.tla:454).
- test_sim_5_1_partition_heal: the per-follower convergence loop was vacuous —
  it bounded by commit_index, which stays 0 for followers under the leader-only
  commit model, so the loop never ran. Bound by log_count instead (followers DO
  advance the replicated log); Log Matching still guarantees the shared-prefix
  terms agree. Now non-vacuous; still passes.

Test/comment-only; no behavior change. Lib suite Ok:1 Fail:0.
This commit is contained in:
Rongsong Shen 2026-06-25 04:38:43 +00:00
parent 0e8b4a12bf
commit 6563adf8c6
2 changed files with 24 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1025,17 +1025,20 @@ void raft_sim_dump_trace(const raft_sim_cluster_t *c, FILE *fp,
*/ */
static const char *sim_tla_action_name(raft_sim_action_kind_t kind) static const char *sim_tla_action_name(raft_sim_action_kind_t kind)
{ {
/* Each return string is verbatim the raft.tla `Next` disjunct name (raft.tla:454);
* no per-case line numbers — they drift as raft.tla evolves and the name IS the
* stable spec reference. */
switch (kind) { switch (kind) {
case RAFT_SIM_ACT_RESTART: return "Restart"; /* raft.tla:166 */ case RAFT_SIM_ACT_RESTART: return "Restart";
case RAFT_SIM_ACT_TIMEOUT: return "Timeout"; /* raft.tla:178 */ case RAFT_SIM_ACT_TIMEOUT: return "Timeout";
case RAFT_SIM_ACT_REQUEST_VOTE: return "RequestVote"; /* raft.tla:190 */ case RAFT_SIM_ACT_REQUEST_VOTE: return "RequestVote";
case RAFT_SIM_ACT_BECOME_LEADER: return "BecomeLeader"; /* raft.tla:229 */ case RAFT_SIM_ACT_BECOME_LEADER: return "BecomeLeader";
case RAFT_SIM_ACT_CLIENT_REQUEST: return "ClientRequest"; /* raft.tla:246 */ case RAFT_SIM_ACT_CLIENT_REQUEST: return "ClientRequest";
case RAFT_SIM_ACT_APPEND_ENTRIES: return "AppendEntries"; /* raft.tla:218 */ case RAFT_SIM_ACT_APPEND_ENTRIES: return "AppendEntries";
case RAFT_SIM_ACT_ADVANCE_COMMIT: return "AdvanceCommitIndex"; /* raft.tla:259 */ case RAFT_SIM_ACT_ADVANCE_COMMIT: return "AdvanceCommitIndex";
case RAFT_SIM_ACT_RECEIVE: return "Receive"; /* raft.tla:421 */ case RAFT_SIM_ACT_RECEIVE: return "Receive";
case RAFT_SIM_ACT_DUPLICATE_MESSAGE: return "DuplicateMessage"; /* raft.tla:443 */ case RAFT_SIM_ACT_DUPLICATE_MESSAGE: return "DuplicateMessage";
case RAFT_SIM_ACT_DROP_MESSAGE: return "DropMessage"; /* raft.tla:448 */ case RAFT_SIM_ACT_DROP_MESSAGE: return "DropMessage";
} }
return "Unknown"; return "Unknown";
} }

17
src/lib/testsuite/test_raft.c
View file

@ -8229,22 +8229,27 @@ static void test_sim_5_1_partition_heal(void)
"post-heal cluster does not have exactly one leader"); "post-heal cluster does not have exactly one leader");
/* Convergence is observable: the leader committed a non-trivial prefix, and /* Convergence is observable: the leader committed a non-trivial prefix, and
* every (formerly-isolated) node's committed entries match the leader's at the * every (formerly-isolated) node's REPLICATED LOG matches the leader's at the
* same index/term over their shared committed prefix. */ * same index/term over their shared log prefix. NOTE: this library uses a
* leader-only commit model (a follower's commit_index does not advance from
* AppendEntries — see Implementation Notes), so followers end at commit_index=0;
* bounding by commit_index would make this loop vacuous. Bound by log_count
* instead, which followers DO advance via replication — Log Matching (asserted
* each step via raft_sim_check_all) guarantees the shared-prefix terms agree. */
TEST_ASSERT_TRUE_MESSAGE(c.nodes[leader_idx].commit_index > 0, TEST_ASSERT_TRUE_MESSAGE(c.nodes[leader_idx].commit_index > 0,
"leader never committed any entry across the scenario"); "leader never committed any entry across the scenario");
for (int i = 0; i < c.n; i++) { for (int i = 0; i < c.n; i++) {
if (i == leader_idx) if (i == leader_idx)
continue; continue;
uint64_t shared = c.nodes[i].commit_index; uint64_t shared = (uint64_t)c.nodes[i].log_count;
if (shared > c.nodes[leader_idx].commit_index) if (shared > (uint64_t)c.nodes[leader_idx].log_count)
shared = c.nodes[leader_idx].commit_index; shared = (uint64_t)c.nodes[leader_idx].log_count;
for (uint64_t e = 1; e <= shared; e++) { for (uint64_t e = 1; e <= shared; e++) {
TEST_ASSERT_EQUAL_UINT64_MESSAGE( TEST_ASSERT_EQUAL_UINT64_MESSAGE(
c.nodes[leader_idx].log[e - 1].term, c.nodes[leader_idx].log[e - 1].term,
c.nodes[i].log[e - 1].term, c.nodes[i].log[e - 1].term,
"formerly-isolated node diverges from leader committed prefix"); "formerly-isolated node diverges from leader's replicated log prefix");
} }
} }
} }