From a38d9a72714d4a3cedaa2127c2cdb910b8feae1e Mon Sep 17 00:00:00 2001 From: Rongsong Shen Date: Wed, 24 Jun 2026 12:51:58 +0000 Subject: [PATCH] feat(raft-sim-conformance): State Machine Safety invariant checker (task 3.4) --- .kiro/specs/raft-sim-conformance/tasks.md | 2 +- src/lib/raft/raft.h | 20 +++++++ src/lib/raft/raft_sim.c | 27 +++++++++ src/lib/testsuite/test_raft.c | 71 +++++++++++++++++++++++ 4 files changed, 119 insertions(+), 1 deletion(-) diff --git a/.kiro/specs/raft-sim-conformance/tasks.md b/.kiro/specs/raft-sim-conformance/tasks.md index f1c04ae..7b6ef3d 100644 --- a/.kiro/specs/raft-sim-conformance/tasks.md +++ b/.kiro/specs/raft-sim-conformance/tasks.md @@ -79,7 +79,7 @@ - _Boundary: raft_sim.c, test_raft.c_ - _Depends: 1.1_ -- [ ] 3.4 RED+GREEN: State Machine Safety checker (P) +- [x] 3.4 RED+GREEN: State Machine Safety checker (P) - Test: divergent `applied[k]` across two nodes fails; identical applied prefixes pass - Implement `raft_sim_check_state_machine_safety` over `applied[]` - Observable completion: both directions assert correctly diff --git a/src/lib/raft/raft.h b/src/lib/raft/raft.h index f940cda..da817c0 100644 --- a/src/lib/raft/raft.h +++ b/src/lib/raft/raft.h @@ -813,6 +813,26 @@ int raft_sim_check_election_safety(const raft_sim_cluster_t *c); */ int raft_sim_check_leader_completeness(const raft_sim_cluster_t *c); +/* + * raft_sim_check_state_machine_safety: assert the Raft State Machine Safety property + * over the cluster's observable per-node applied state (Req 3.4, 3.6). + * + * State Machine Safety: no two nodes have applied DIFFERENT values at the same log + * index. Computed purely from observable state (Req 3.6): each node's applied extent + * is 1..commit_index (sim_conf_on_commit_advanced fills applied[k-1] with the value + * applied at 1-based committed index k). For every pair (a < b) and every index k in + * the shared applied prefix 1..min(a->commit_index, b->commit_index), the property is + * violated if applied[k-1] differs between the two nodes. Pairs are symmetric, so + * a < b suffices. + * + * Returns 1 if State Machine Safety holds across the whole cluster, 0 if any pair of + * nodes disagrees on the value applied at a commonly-applied index. Pure read-only + * over c (reads applied[] and commit_index only; no I/O, no Unity assertions) so the + * lib stays test-framework-agnostic; the caller asserts on the returned value (same + * convention as raft_sim_check_log_matching). + */ +int raft_sim_check_state_machine_safety(const raft_sim_cluster_t *c); + /* * raft_sim_advance_commit: drive raft_advance_commit on node_idx (task 6.1). * diff --git a/src/lib/raft/raft_sim.c b/src/lib/raft/raft_sim.c index 3805697..a7c18b4 100644 --- a/src/lib/raft/raft_sim.c +++ b/src/lib/raft/raft_sim.c @@ -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) diff --git a/src/lib/testsuite/test_raft.c b/src/lib/testsuite/test_raft.c index c7197e9..f274017 100644 --- a/src/lib/testsuite/test_raft.c +++ b/src/lib/testsuite/test_raft.c @@ -3824,6 +3824,75 @@ static void test_sim_check_leader_completeness_pass_when_present(void) TEST_ASSERT_EQUAL_INT(1, raft_sim_check_leader_completeness(&c)); } +/* + * test_sim_check_state_machine_safety_fail_on_divergence (task 3.4; Req 3.4, 3.6) + * + * State Machine Safety: no two nodes may have applied DIFFERENT values at the same + * (1-based) log index within their common applied prefix (1..min(commit_index)). + * Hand-build two nodes that both committed index 2 but applied DIFFERENT values at + * index 2 ⇒ the checker must FAIL (0). The applied extent per node is commit_index + * (sim_conf_on_commit_advanced fills applied[1..commit_index]); applied[k-1] is the + * value applied at 1-based index k. (Hand-set applied[]/commit_index directly — a + * checker unit test over a hand-built cluster, not a protocol run.) + */ +static void test_sim_check_state_machine_safety_fail_on_divergence(void) +{ + raft_sim_cluster_t c; + memset(&c, 0, sizeof(c)); + + TEST_ASSERT_EQUAL_INT(0, raft_sim_init(&c, 3, 2000)); + + /* Both node 0 and node 1 committed (applied) indices 1..2. They AGREE at + * index 1 (value 10) but DISAGREE at index 2 (30 vs 99) ⇒ violation at a + * shared applied index. */ + c.nodes[0].commit_index = 2; + c.nodes[0].applied[0] = 10; + c.nodes[0].applied[1] = 30; + + c.nodes[1].commit_index = 2; + c.nodes[1].applied[0] = 10; + c.nodes[1].applied[1] = 99; /* differs from node 0 at index 2 */ + + TEST_ASSERT_EQUAL_INT(0, raft_sim_check_state_machine_safety(&c)); +} + +/* + * test_sim_check_state_machine_safety_pass_on_agreement (task 3.4; Req 3.4, 3.6) + * + * State Machine Safety holds when every pair of nodes agrees on applied values + * across their COMMON applied prefix. Two scenarios pass: + * (a) two nodes with identical applied[] over equal commit extents (both [10,20]); + * (b) nodes with DIFFERENT commit extents but identical values over the SHARED + * prefix (node0 [10,20,30] @commit 3 vs node1 [10,20] @commit 2 ⇒ shared + * prefix 1..2 is identical ⇒ holds; index 3 is not applied by node1). + */ +static void test_sim_check_state_machine_safety_pass_on_agreement(void) +{ + raft_sim_cluster_t c; + memset(&c, 0, sizeof(c)); + + TEST_ASSERT_EQUAL_INT(0, raft_sim_init(&c, 3, 2000)); + + /* (a) Identical applied[] over equal commit extents. */ + c.nodes[0].commit_index = 2; + c.nodes[0].applied[0] = 10; + c.nodes[0].applied[1] = 20; + + c.nodes[1].commit_index = 2; + c.nodes[1].applied[0] = 10; + c.nodes[1].applied[1] = 20; + + TEST_ASSERT_EQUAL_INT(1, raft_sim_check_state_machine_safety(&c)); + + /* (b) Different commit extents, identical over the shared prefix 1..2. Node 0 + * has applied one extra index (3 -> 30) that node 1 has not committed; the + * shared prefix still agrees ⇒ holds. */ + c.nodes[0].commit_index = 3; + c.nodes[0].applied[2] = 30; + + TEST_ASSERT_EQUAL_INT(1, raft_sim_check_state_machine_safety(&c)); +} + /* ---------- Group: Simulator invariant tests (tasks 9.1-9.4) ---------- * * These are observation-based invariant tests. They drive the COMPLETE @@ -7561,6 +7630,8 @@ void test_raft(void) RUN_TEST(test_sim_check_election_safety_pass_on_single_leader); RUN_TEST(test_sim_check_leader_completeness_fail_on_missing_committed); RUN_TEST(test_sim_check_leader_completeness_pass_when_present); + RUN_TEST(test_sim_check_state_machine_safety_fail_on_divergence); + RUN_TEST(test_sim_check_state_machine_safety_pass_on_agreement); RUN_TEST(test_sim_9_1_replication_and_partition_catch_up); RUN_TEST(test_sim_9_2_divergent_suffix_truncation); RUN_TEST(test_sim_9_3_drop_dup_reorder_convergence);