forked from lei.chen/myxce
feat(raft-sim-conformance): raft_sim_check_all first-failure composition (task 3.5)
This commit is contained in:
parent
a38d9a7271
commit
f0be46fb32
4 changed files with 171 additions and 1 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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).
|
||||
*
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue