From 6563adf8c64fa883e0a58b73fd6ae0fd55ac4e7a Mon Sep 17 00:00:00 2001 From: Rongsong Shen Date: Thu, 25 Jun 2026 04:38:43 +0000 Subject: [PATCH] docs(raft-sim-conformance): cosmetic cleanups (LOW review nits) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 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. --- src/lib/raft/raft_sim.c | 23 +++++++++++++---------- src/lib/testsuite/test_raft.c | 17 +++++++++++------ 2 files changed, 24 insertions(+), 16 deletions(-) diff --git a/src/lib/raft/raft_sim.c b/src/lib/raft/raft_sim.c index 1adbee26..4dd54d88 100644 --- a/src/lib/raft/raft_sim.c +++ b/src/lib/raft/raft_sim.c @@ -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) { + /* 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) { - case RAFT_SIM_ACT_RESTART: return "Restart"; /* raft.tla:166 */ - case RAFT_SIM_ACT_TIMEOUT: return "Timeout"; /* raft.tla:178 */ - case RAFT_SIM_ACT_REQUEST_VOTE: return "RequestVote"; /* raft.tla:190 */ - case RAFT_SIM_ACT_BECOME_LEADER: return "BecomeLeader"; /* raft.tla:229 */ - case RAFT_SIM_ACT_CLIENT_REQUEST: return "ClientRequest"; /* raft.tla:246 */ - case RAFT_SIM_ACT_APPEND_ENTRIES: return "AppendEntries"; /* raft.tla:218 */ - case RAFT_SIM_ACT_ADVANCE_COMMIT: return "AdvanceCommitIndex"; /* raft.tla:259 */ - case RAFT_SIM_ACT_RECEIVE: return "Receive"; /* raft.tla:421 */ - case RAFT_SIM_ACT_DUPLICATE_MESSAGE: return "DuplicateMessage"; /* raft.tla:443 */ - case RAFT_SIM_ACT_DROP_MESSAGE: return "DropMessage"; /* raft.tla:448 */ + case RAFT_SIM_ACT_RESTART: return "Restart"; + case RAFT_SIM_ACT_TIMEOUT: return "Timeout"; + case RAFT_SIM_ACT_REQUEST_VOTE: return "RequestVote"; + case RAFT_SIM_ACT_BECOME_LEADER: return "BecomeLeader"; + case RAFT_SIM_ACT_CLIENT_REQUEST: return "ClientRequest"; + case RAFT_SIM_ACT_APPEND_ENTRIES: return "AppendEntries"; + case RAFT_SIM_ACT_ADVANCE_COMMIT: return "AdvanceCommitIndex"; + case RAFT_SIM_ACT_RECEIVE: return "Receive"; + case RAFT_SIM_ACT_DUPLICATE_MESSAGE: return "DuplicateMessage"; + case RAFT_SIM_ACT_DROP_MESSAGE: return "DropMessage"; } return "Unknown"; } diff --git a/src/lib/testsuite/test_raft.c b/src/lib/testsuite/test_raft.c index c3b8bc2c..def2b223 100644 --- a/src/lib/testsuite/test_raft.c +++ b/src/lib/testsuite/test_raft.c @@ -8229,22 +8229,27 @@ static void test_sim_5_1_partition_heal(void) "post-heal cluster does not have exactly one leader"); /* Convergence is observable: the leader committed a non-trivial prefix, and - * every (formerly-isolated) node's committed entries match the leader's at the - * same index/term over their shared committed prefix. */ + * every (formerly-isolated) node's REPLICATED LOG matches the leader's at the + * 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, "leader never committed any entry across the scenario"); for (int i = 0; i < c.n; i++) { if (i == leader_idx) continue; - uint64_t shared = c.nodes[i].commit_index; - if (shared > c.nodes[leader_idx].commit_index) - shared = c.nodes[leader_idx].commit_index; + uint64_t shared = (uint64_t)c.nodes[i].log_count; + if (shared > (uint64_t)c.nodes[leader_idx].log_count) + shared = (uint64_t)c.nodes[leader_idx].log_count; for (uint64_t e = 1; e <= shared; e++) { TEST_ASSERT_EQUAL_UINT64_MESSAGE( c.nodes[leader_idx].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"); } } }