From f0be46fb324bf7f0a1ac3038d7ceee24e970e604 Mon Sep 17 00:00:00 2001 From: Rongsong Shen Date: Wed, 24 Jun 2026 13:00:10 +0000 Subject: [PATCH] feat(raft-sim-conformance): raft_sim_check_all first-failure composition (task 3.5) --- .kiro/specs/raft-sim-conformance/tasks.md | 2 +- src/lib/raft/raft.h | 36 ++++++++ src/lib/raft/raft_sim.c | 28 ++++++ src/lib/testsuite/test_raft.c | 106 ++++++++++++++++++++++ 4 files changed, 171 insertions(+), 1 deletion(-) diff --git a/.kiro/specs/raft-sim-conformance/tasks.md b/.kiro/specs/raft-sim-conformance/tasks.md index 7b6ef3d..30a402e 100644 --- a/.kiro/specs/raft-sim-conformance/tasks.md +++ b/.kiro/specs/raft-sim-conformance/tasks.md @@ -87,7 +87,7 @@ - _Boundary: raft_sim.c, test_raft.c_ - _Depends: 1.1_ -- [ ] 3.5 RED+GREEN: `raft_sim_check_all` returns the first failing invariant and halts +- [x] 3.5 RED+GREEN: `raft_sim_check_all` returns the first failing invariant and halts - Test: a cluster violating two invariants reports the first; a clean cluster returns OK - Implement `raft_sim_check_all` composing 3.1–3.4 in a fixed order - Observable completion: first-failure semantics verified diff --git a/src/lib/raft/raft.h b/src/lib/raft/raft.h index da817c0..d61e6d9 100644 --- a/src/lib/raft/raft.h +++ b/src/lib/raft/raft.h @@ -833,6 +833,42 @@ int raft_sim_check_leader_completeness(const raft_sim_cluster_t *c); */ int raft_sim_check_state_machine_safety(const raft_sim_cluster_t *c); +/* + * raft_sim_invariant_t: identifier for the four Raft safety invariants checked by + * the conformance harness, in the FIXED evaluation order used by + * raft_sim_check_all (Req 3.5). RAFT_SIM_INV_NONE (0) means "all invariants hold". + * The ordinal order mirrors the requirements/design listing so the trace dumper + * (task 4.1) and scheduler (task 4.2) can report the failing invariant by name. + */ +typedef enum { + RAFT_SIM_INV_NONE = 0, /* all four invariants hold */ + RAFT_SIM_INV_ELECTION_SAFETY, /* 1: raft_sim_check_election_safety */ + RAFT_SIM_INV_LOG_MATCHING, /* 2: raft_sim_check_log_matching */ + RAFT_SIM_INV_LEADER_COMPLETENESS, /* 3: raft_sim_check_leader_completeness */ + RAFT_SIM_INV_STATE_MACHINE_SAFETY,/* 4: raft_sim_check_state_machine_safety */ +} raft_sim_invariant_t; + +/* + * raft_sim_check_all: evaluate the four Raft safety invariants over the cluster in + * the FIXED order (1) Election Safety, (2) Log Matching, (3) Leader Completeness, + * (4) State Machine Safety, and return the identifier of the FIRST one that is + * violated (Req 3.5 — "halt the run immediately and report the failing invariant"). + * + * Short-circuits: once a checker reports a violation, later checkers are NOT + * evaluated, so the reported "first failing invariant" is deterministic. Returns + * RAFT_SIM_INV_NONE (0) when every invariant holds. Pure read-only over c (no I/O, + * no Unity assertions) so the lib stays test-framework-agnostic; the caller (trace + * dumper / scheduler) consumes the returned identity. + */ +raft_sim_invariant_t raft_sim_check_all(const raft_sim_cluster_t *c); + +/* + * raft_sim_invariant_name: human-readable name for a raft_sim_invariant_t, for the + * trace dumper (task 4.1) and scheduler diagnostics. Returns a static string; never + * NULL (an out-of-range value maps to "unknown"). + */ +const char *raft_sim_invariant_name(raft_sim_invariant_t inv); + /* * 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 a7c18b4..173e04d 100644 --- a/src/lib/raft/raft_sim.c +++ b/src/lib/raft/raft_sim.c @@ -909,6 +909,34 @@ int raft_sim_check_state_machine_safety(const raft_sim_cluster_t *c) return 1; /* holds */ } +raft_sim_invariant_t raft_sim_check_all(const raft_sim_cluster_t *c) +{ + /* Evaluate the four invariants in the FIXED order required by Req 3.5 and + * short-circuit on the FIRST violation, so the reported failing invariant is + * deterministic. Each checker returns 1=holds / 0=violated. */ + if (!raft_sim_check_election_safety(c)) + return RAFT_SIM_INV_ELECTION_SAFETY; + if (!raft_sim_check_log_matching(c)) + return RAFT_SIM_INV_LOG_MATCHING; + if (!raft_sim_check_leader_completeness(c)) + return RAFT_SIM_INV_LEADER_COMPLETENESS; + if (!raft_sim_check_state_machine_safety(c)) + return RAFT_SIM_INV_STATE_MACHINE_SAFETY; + return RAFT_SIM_INV_NONE; /* all four hold */ +} + +const char *raft_sim_invariant_name(raft_sim_invariant_t inv) +{ + switch (inv) { + case RAFT_SIM_INV_NONE: return "none"; + case RAFT_SIM_INV_ELECTION_SAFETY: return "election-safety"; + case RAFT_SIM_INV_LOG_MATCHING: return "log-matching"; + case RAFT_SIM_INV_LEADER_COMPLETENESS: return "leader-completeness"; + case RAFT_SIM_INV_STATE_MACHINE_SAFETY: return "state-machine-safety"; + } + return "unknown"; +} + 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 f274017..21fb2f3 100644 --- a/src/lib/testsuite/test_raft.c +++ b/src/lib/testsuite/test_raft.c @@ -3893,6 +3893,109 @@ static void test_sim_check_state_machine_safety_pass_on_agreement(void) TEST_ASSERT_EQUAL_INT(1, raft_sim_check_state_machine_safety(&c)); } +/* + * test_sim_check_all_first_failure_is_election_safety (task 3.5; Req 3.5) + * + * raft_sim_check_all evaluates the four invariants in a FIXED ORDER — + * (1) Election Safety, (2) Log Matching, (3) Leader Completeness, + * (4) State Machine Safety — and returns the identifier of the FIRST one that + * is violated, short-circuiting before later checkers run. Hand-build a cluster + * that violates TWO invariants: Election Safety (earliest in order) AND State + * Machine Safety (latest). The composer must report ELECTION_SAFETY (the first + * in fixed order), NOT the later State Machine Safety violation — proving + * deterministic first-failure ordering. + */ +static void test_sim_check_all_first_failure_is_election_safety(void) +{ + raft_sim_cluster_t c; + memset(&c, 0, sizeof(c)); + + TEST_ASSERT_EQUAL_INT(0, raft_sim_init(&c, 3, 2000)); + + /* Violation 1 (Election Safety): two LEADERs at the SAME term 7. */ + c.nodes[0].state.role = RAFT_LEADER; + c.nodes[0].state.term = 7; + c.nodes[1].state.role = RAFT_LEADER; + c.nodes[1].state.term = 7; + c.nodes[2].state.role = RAFT_FOLLOWER; + c.nodes[2].state.term = 7; + + /* Violation 2 (State Machine Safety): nodes 0 and 1 applied DIFFERENT + * values at the shared committed index 1. */ + c.nodes[0].commit_index = 1; + c.nodes[0].applied[0] = 10; + c.nodes[1].commit_index = 1; + c.nodes[1].applied[0] = 99; + + /* Election Safety is first in the fixed order ⇒ the composer reports it and + * never reaches the State Machine Safety check. */ + TEST_ASSERT_EQUAL_INT(RAFT_SIM_INV_ELECTION_SAFETY, raft_sim_check_all(&c)); +} + +/* + * test_sim_check_all_reaches_later_invariant (task 3.5; Req 3.5) + * + * When all earlier invariants hold, the composer must reach and report a + * later-in-order violation. Hand-build a cluster that violates ONLY State + * Machine Safety (the LAST checker) — Election Safety, Log Matching, and Leader + * Completeness all hold. The composer must return STATE_MACHINE_SAFETY, proving + * the later checkers are actually evaluated once the earlier ones pass. + */ +static void test_sim_check_all_reaches_later_invariant(void) +{ + raft_sim_cluster_t c; + memset(&c, 0, sizeof(c)); + + TEST_ASSERT_EQUAL_INT(0, raft_sim_init(&c, 3, 2000)); + + /* No two same-term leaders (Election Safety holds): no leaders at all. */ + /* Logs empty ⇒ Log Matching trivially holds; no leaders ⇒ Leader + * Completeness trivially holds. Only divergent applied[] at shared index 1 + * violates State Machine Safety. */ + c.nodes[0].commit_index = 1; + c.nodes[0].applied[0] = 10; + c.nodes[1].commit_index = 1; + c.nodes[1].applied[0] = 99; /* differs from node 0 at index 1 */ + + TEST_ASSERT_EQUAL_INT(RAFT_SIM_INV_STATE_MACHINE_SAFETY, + raft_sim_check_all(&c)); +} + +/* + * test_sim_check_all_clean_returns_none (task 3.5; Req 3.5) + * + * A cluster with no violations of any invariant ⇒ raft_sim_check_all returns + * RAFT_SIM_INV_NONE (0). A freshly-initialised cluster (no leaders, empty logs, + * nothing committed) satisfies all four invariants trivially. + */ +static void test_sim_check_all_clean_returns_none(void) +{ + raft_sim_cluster_t c; + memset(&c, 0, sizeof(c)); + + TEST_ASSERT_EQUAL_INT(0, raft_sim_init(&c, 3, 2000)); + + /* One clean LEADER, agreeing logs and applied prefix ⇒ everything holds. */ + c.nodes[0].state.role = RAFT_LEADER; + c.nodes[0].state.term = 5; + c.nodes[0].log[0].term = 5; + c.nodes[0].log_count = 1; + c.nodes[0].commit_index = 1; + c.nodes[0].applied[0] = 42; + + c.nodes[1].state.role = RAFT_FOLLOWER; + c.nodes[1].state.term = 5; + c.nodes[1].log[0].term = 5; + c.nodes[1].log_count = 1; + c.nodes[1].commit_index = 1; + c.nodes[1].applied[0] = 42; + + c.nodes[2].state.role = RAFT_FOLLOWER; + c.nodes[2].state.term = 5; + + TEST_ASSERT_EQUAL_INT(RAFT_SIM_INV_NONE, raft_sim_check_all(&c)); +} + /* ---------- Group: Simulator invariant tests (tasks 9.1-9.4) ---------- * * These are observation-based invariant tests. They drive the COMPLETE @@ -7632,6 +7735,9 @@ void test_raft(void) 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_check_all_first_failure_is_election_safety); + RUN_TEST(test_sim_check_all_reaches_later_invariant); + RUN_TEST(test_sim_check_all_clean_returns_none); 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);