feat(raft-sim-conformance): raft_sim_run + deterministic replay (task 4.4)
This commit is contained in:
parent
5f67be4fa3
commit
b844e75f3b
4 changed files with 157 additions and 1 deletions
|
|
@ -121,7 +121,7 @@
|
|||
- _Boundary: raft_sim.c, test_raft.c_
|
||||
- _Depends: 4.2_
|
||||
|
||||
- [ ] 4.4 RED+GREEN: deterministic replay from `(n, seed, max_steps)`
|
||||
- [x] 4.4 RED+GREEN: deterministic replay from `(n, seed, max_steps)`
|
||||
- Test: two runs with the same `(n, seed, max_steps)` reach identical final per-node + bag state and an identical recorded trace
|
||||
- Implement `raft_sim_run(c, max_steps)` and confirm no wall-clock/address/uninitialized input leaks into choices
|
||||
- Observable completion: byte-identical replay verified across two runs
|
||||
|
|
|
|||
|
|
@ -954,6 +954,23 @@ int raft_sim_restart_node(raft_sim_cluster_t *c, int node_idx);
|
|||
*/
|
||||
int raft_sim_step(raft_sim_cluster_t *c);
|
||||
|
||||
/*
|
||||
* raft_sim_run: drive up to `max_steps` raft_sim_step actions through the library
|
||||
* (raft-sim-conformance task 4.4; Req 1.5, 1.6, 5.3).
|
||||
*
|
||||
* Loops raft_sim_step. On the FIRST step that reports an invariant violation
|
||||
* (returns < 0), STOPS immediately and returns that same < 0 value (the step
|
||||
* already dumped the replayable trace to stderr) — the "halt on first violation"
|
||||
* contract (Req 3.5/5.3). If all `max_steps` complete with no violation, returns 0.
|
||||
*
|
||||
* Determinism: every nondeterministic choice flows from c->prng (seeded from
|
||||
* c->seed in raft_sim_conformance_init), so two clusters initialized with the same
|
||||
* (n, election_timeout, seed) and run for the same `max_steps` reach byte-identical
|
||||
* observable state and an identical recorded trace — deterministic replay (Req 1.6).
|
||||
* No wall-clock, address, or uninitialized input ever feeds a choice (Req 1.5).
|
||||
*/
|
||||
int raft_sim_run(raft_sim_cluster_t *c, int max_steps);
|
||||
|
||||
#endif /* XCE_TESTING */
|
||||
|
||||
#endif /* RAFT_H */
|
||||
|
|
|
|||
|
|
@ -1249,4 +1249,23 @@ int raft_sim_step(raft_sim_cluster_t *c)
|
|||
return 0;
|
||||
}
|
||||
|
||||
/* ---------- multi-step run driver (raft-sim-conformance task 4.4) ---------- */
|
||||
|
||||
int raft_sim_run(raft_sim_cluster_t *c, int max_steps)
|
||||
{
|
||||
/* Bounded loop of single steps. raft_sim_step is the SOLE consumer of c->prng,
|
||||
* so a run is a pure deterministic function of (n, seed) and the step count —
|
||||
* two same-keyed clusters produce identical traces and final state (R1.5/1.6/
|
||||
* 5.3). Halt on the FIRST violation: raft_sim_step returns < 0 and has already
|
||||
* dumped the replayable trace, so propagate that value unchanged (R3.5). A clean
|
||||
* exhaustion of the step budget returns 0. */
|
||||
for (int step = 0; step < max_steps; step++) {
|
||||
int rc = raft_sim_step(c);
|
||||
if (rc < 0)
|
||||
return rc; /* first invariant violation — stop and surface it */
|
||||
}
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
||||
#endif /* XCE_TESTING */
|
||||
|
|
|
|||
|
|
@ -7961,6 +7961,125 @@ static void test_sim_4_3_restart_preserves_persistence(void)
|
|||
/* The restart ALONE produces no invariant violation (Req 2.1). */
|
||||
TEST_ASSERT_EQUAL_INT(RAFT_SIM_INV_NONE, raft_sim_check_all(&c));
|
||||
}
|
||||
|
||||
/*
|
||||
* sim_assert_clusters_identical: assert two conformance clusters are BYTE-IDENTICAL
|
||||
* in every observable replay-state field (the deterministic-replay oracle for task
|
||||
* 4.4). Compares the recorded trace, the message bag, the PRNG state, and every
|
||||
* per-node durable + applied + consensus field. Any divergence here means a
|
||||
* wall-clock / address / uninitialized input leaked into a scheduler choice (R1.5),
|
||||
* which would break same-seed replay (R1.6/5.3).
|
||||
*/
|
||||
static void sim_assert_clusters_identical(const raft_sim_cluster_t *a,
|
||||
const raft_sim_cluster_t *b)
|
||||
{
|
||||
/* Same shape. */
|
||||
TEST_ASSERT_EQUAL_INT(a->n, b->n);
|
||||
|
||||
/* Identical recorded trace (same length AND same bytes — R1.6/5.3). */
|
||||
TEST_ASSERT_EQUAL_INT(a->trace_len, b->trace_len);
|
||||
TEST_ASSERT_EQUAL_INT(0,
|
||||
memcmp(a->trace, b->trace,
|
||||
(size_t)a->trace_len * sizeof(raft_sim_action_t)));
|
||||
|
||||
/* Identical in-flight message bag (same count AND same bytes). */
|
||||
TEST_ASSERT_EQUAL_INT(a->bag_count, b->bag_count);
|
||||
TEST_ASSERT_EQUAL_INT(0,
|
||||
memcmp(a->bag, b->bag,
|
||||
(size_t)a->bag_count * sizeof(raft_sim_msg_t)));
|
||||
|
||||
/* Identical PRNG state: the single source of nondeterminism ended at the same
|
||||
* point, so every choice consumed exactly the same random stream. */
|
||||
TEST_ASSERT_EQUAL_UINT64(a->seed, b->seed);
|
||||
TEST_ASSERT_EQUAL_UINT64(a->prng, b->prng);
|
||||
|
||||
/* Per-node observable state: durable log, commit/applied, and consensus role/
|
||||
* term/votedFor read from the node's snapshot. */
|
||||
for (int i = 0; i < a->n; i++) {
|
||||
const raft_sim_node_t *na = &a->nodes[i];
|
||||
const raft_sim_node_t *nb = &b->nodes[i];
|
||||
|
||||
TEST_ASSERT_EQUAL_INT(na->log_count, nb->log_count);
|
||||
for (int k = 0; k < na->log_count; k++) {
|
||||
TEST_ASSERT_EQUAL_UINT64(na->log[k].term, nb->log[k].term);
|
||||
TEST_ASSERT_EQUAL_UINT(na->log[k].len, nb->log[k].len);
|
||||
TEST_ASSERT_EQUAL_INT(0,
|
||||
memcmp(na->log[k].bytes, nb->log[k].bytes, na->log[k].len));
|
||||
}
|
||||
|
||||
TEST_ASSERT_EQUAL_UINT64(na->commit_index, nb->commit_index);
|
||||
TEST_ASSERT_EQUAL_INT(na->commit_advanced_count, nb->commit_advanced_count);
|
||||
|
||||
uint64_t shared = na->commit_index;
|
||||
if (shared > RAFT_SIM_MAX_LOG)
|
||||
shared = RAFT_SIM_MAX_LOG;
|
||||
for (uint64_t k = 1; k <= shared; k++)
|
||||
TEST_ASSERT_EQUAL_UINT64(na->applied[k - 1], nb->applied[k - 1]);
|
||||
|
||||
raft_snapshot_t sa, sb;
|
||||
raft_snapshot(&na->state, &sa);
|
||||
raft_snapshot(&nb->state, &sb);
|
||||
TEST_ASSERT_EQUAL_UINT64(sa.term, sb.term);
|
||||
TEST_ASSERT_EQUAL_INT((int)sa.role, (int)sb.role);
|
||||
TEST_ASSERT_EQUAL_INT(sa.voted_for, sb.voted_for);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
* test_sim_4_4_run_deterministic_replay (raft-sim-conformance task 4.4; Req 1.5, 1.6,
|
||||
* 5.3)
|
||||
*
|
||||
* raft_sim_run(c, max_steps) loops raft_sim_step up to max_steps, halting (and
|
||||
* returning < 0) on the first invariant violation, returning 0 on a clean run.
|
||||
* Deterministic replay: two clusters initialized with the SAME (n, election_timeout,
|
||||
* seed) and run for the SAME max_steps MUST reach byte-identical observable state and
|
||||
* an identical recorded trace. The library is correct (bug-1095/1096 fixed), so each
|
||||
* run returns 0; identical replay across the pair proves no wall-clock / address /
|
||||
* uninitialized input leaked into any scheduler choice (R1.5/1.6/5.3).
|
||||
*
|
||||
* Steps/nodes are bounded (3 nodes, 400 steps over a few seeds) to stay within the
|
||||
* lib suite time budget.
|
||||
*/
|
||||
static void test_sim_4_4_run_deterministic_replay(void)
|
||||
{
|
||||
/* Several seeds, each run twice — proving the property holds across seeds, not
|
||||
* just one. Seeds known to drive the correct library to a clean (no-violation)
|
||||
* run while still electing a leader and replicating. */
|
||||
static const uint64_t seeds[] = { 3ULL, 0x4A33ULL, 1ULL };
|
||||
const int N = 3;
|
||||
const int MAX_STEPS = 400;
|
||||
|
||||
for (size_t s = 0; s < sizeof(seeds) / sizeof(seeds[0]); s++) {
|
||||
uint64_t seed = seeds[s];
|
||||
|
||||
raft_sim_cluster_t a, b;
|
||||
memset(&a, 0, sizeof(a));
|
||||
memset(&b, 0, sizeof(b));
|
||||
|
||||
TEST_ASSERT_EQUAL_INT(0, raft_sim_conformance_init(&a, N, 2000, seed));
|
||||
TEST_ASSERT_EQUAL_INT(0, raft_sim_conformance_init(&b, N, 2000, seed));
|
||||
|
||||
int ra = raft_sim_run(&a, MAX_STEPS);
|
||||
int rb = raft_sim_run(&b, MAX_STEPS);
|
||||
|
||||
/* Correct library: a healthy run completes with no invariant violation.
|
||||
* A < 0 here is a REAL divergence the harness surfaced (the step already
|
||||
* dumped the replayable trace to stderr) — NOT something to mask. */
|
||||
TEST_ASSERT_TRUE_MESSAGE(ra == 0,
|
||||
"raft_sim_run surfaced an invariant violation on the correct library (run a)");
|
||||
TEST_ASSERT_TRUE_MESSAGE(rb == 0,
|
||||
"raft_sim_run surfaced an invariant violation on the correct library (run b)");
|
||||
|
||||
/* Same seed + n + max_steps ⇒ identical run outcome and identical final
|
||||
* observable state + recorded trace (R1.6/5.3). */
|
||||
TEST_ASSERT_EQUAL_INT(ra, rb);
|
||||
sim_assert_clusters_identical(&a, &b);
|
||||
|
||||
/* The run actually did work (the trace recorded steps), so the byte-identity
|
||||
* above is non-vacuous. */
|
||||
TEST_ASSERT_TRUE(a.trace_len > 0);
|
||||
}
|
||||
}
|
||||
#endif /* XCE_TESTING */
|
||||
|
||||
/* ---------- test_raft entry point ---------- */
|
||||
|
|
@ -8170,6 +8289,7 @@ void test_raft(void)
|
|||
RUN_TEST(test_sim_4_2_step_liveness_and_coverage);
|
||||
RUN_TEST(test_sim_4_2_step_halts_on_forced_violation);
|
||||
RUN_TEST(test_sim_4_3_restart_preserves_persistence);
|
||||
RUN_TEST(test_sim_4_4_run_deterministic_replay);
|
||||
|
||||
/* Group A: basic election correctness (task 5.1) */
|
||||
RUN_TEST(test_proto_A1_single_node_self_elects);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue