lei.chen/myxce
1
0
Fork 1
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(raft-apply-decoupling): task 7.1 apply-ordering conformance assertions

Browse source 
Extend raft_sim.c's deterministic TLA+-conformance harness with two
fault-injectable checks: no reaction before commit, and idempotent
re-apply of an already-committed entry. Wired as dedicated tests only,
not into raft_sim_check_all's fixed four-invariant contract (owned by
a separate spec). RED/GREEN independently verified by adversarial
review; zero regression to existing scenario functions.
This commit is contained in:
Rongsong Shen 2026-07-05 05:25:32 +00:00
parent 2de410c877
commit 5f98d1b0ef
4 changed files with 347 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

75
src/lib/raft/raft.h
View file

@ -467,9 +467,24 @@ void raft_snapshot(const raft_state_t *s, raft_snapshot_t *snap);
* supplied term (emulates G1: entries carry term 0 so on_get_entry_term cannot
* distinguish same-index/different-term entries).
* - RAFT_SIM_BREAK_TRUNCATE: on_truncate_from is a no-op (emulates G3: a divergent
* suffix is never deleted). */
* suffix is never deleted).
* - RAFT_SIM_BREAK_APPLY_BEFORE_COMMIT (raft-apply-decoupling task 7.1):
* on_persist_entry ALSO eagerly decodes and writes the entry's value into
* applied[] at persist time, before the entry ever commits — emulating an
* apply-before-commit regression (the defect class raft-apply-decoupling
* fixes). Lets the new raft_sim_check_apply_after_commit oracle be proven
* sensitive, not merely vacuously passing.
* - RAFT_SIM_BREAK_REAPPLY_GUARD (raft-apply-decoupling task 7.1):
* on_commit_advanced (conformance variant) reprocesses the FULL committed
* prefix on every call instead of only the newly-committed suffix, so a
* forced replay (raft_sim_replay_commit) re-fires an already-applied
* entry's reaction — emulating a duplicate/retried commit notification
* that is not idempotent. Lets the new raft_sim_check_idempotent_reapply
* oracle be proven sensitive. */
#define RAFT_SIM_BREAK_TERM_STAMP 0x1u
#define RAFT_SIM_BREAK_TRUNCATE 0x2u
#define RAFT_SIM_BREAK_APPLY_BEFORE_COMMIT 0x4u
#define RAFT_SIM_BREAK_REAPPLY_GUARD 0x8u
/* Buffered RPC entry: one pending vote-request to route.
* last_log_term/last_log_index capture the CANDIDATE's advertised last-log tuple
@ -614,6 +629,15 @@ typedef struct {
* satisfies the design's `log_len` requirement for the in-memory log length;
* no separate log_len field is added (it would duplicate log_count). */
uint64_t applied[RAFT_SIM_MAX_LOG];
/* apply_reaction_count[k-1] counts how many times committed index k's
* apply-time reaction has fired (raft-apply-decoupling task 7.1). Under
* correct behavior this is always 0 or 1 per index — a value > 1 means the
* SAME committed entry's mutation/reaction ran more than once (a genuine
* duplicate application), which raft_sim_check_idempotent_reapply asserts
* never happens (Req 10.3). Incremented alongside applied[] inside
* sim_conf_on_commit_advanced only; the legacy (non-conformance) adapter
* never touches it, so it stays all-zero for raft_sim_init clusters. */
int apply_reaction_count[RAFT_SIM_MAX_LOG];
/* Persisted-(term, votedFor) shadow surviving a Restart, mirroring raft.tla's
* `Restart` (keeps currentTerm/votedFor/log, resets volatile state). The
* conformance restart action restores from this shadow rather than re-reading
@ -855,6 +879,41 @@ 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);
/* ---- additive apply-ordering assertions (raft-apply-decoupling task 7.1) ----
*
* The two checks below are layered ADDITIONS to the conformance harness's existing
* apply-after-on_commit_advanced loop (sim_conf_on_commit_advanced): they verify
* Req 10.1 and 10.3 against the harness's own apply model (applied[] /
* apply_reaction_count[]). They are deliberately NOT members of raft_sim_invariant_t
* and are NOT evaluated by raft_sim_check_all — that enum/function's four-invariant
* FIXED order is the raft.tla safety-property contract (Req 3.5) and is left
* untouched. Callers assert on these return values directly, same 1=holds/0=violated
* convention as the four checks above. */
/*
* raft_sim_check_apply_after_commit (Req 10.1): assert that no entry's state
* mutation/reaction — the harness's apply model, node->applied[] — occurs before
* that entry commits (node->commit_index reaching its index). applied[] uses the
* same zero-means-absent convention already established for log-entry terms
* elsewhere in this file: an untouched slot reads exactly 0, and every value this
* harness's tests/scheduler ever apply (PRNG draws or hand-authored client values)
* is non-zero, so "applied[k-1] != 0" reliably means "index k has been applied".
* Returns 1 when, for every node and every index k, applied[k-1] != 0 implies
* k <= commit_index; 0 on the first violation. Pure read-only over c.
*/
int raft_sim_check_apply_after_commit(const raft_sim_cluster_t *c);
/*
* raft_sim_check_idempotent_reapply (Req 10.3): assert that re-applying an
* already-committed entry — whether a genuine duplicate on_commit_advanced fire or
* a forced raft_sim_replay_commit retry — never re-executes that entry's apply-time
* mutation/reaction. Backed by node->apply_reaction_count[k-1], incremented once
* per genuine apply of committed index k. Returns 1 when, for every node and every
* index k, apply_reaction_count[k-1] <= 1; 0 on the first index whose reaction
* fired more than once. Pure read-only over c.
*/
int raft_sim_check_idempotent_reapply(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
@ -952,6 +1011,20 @@ void raft_sim_export_trace(const raft_sim_cluster_t *c, FILE *fp);
*/
void raft_sim_advance_commit(raft_sim_cluster_t *c, int node_idx);
/*
* raft_sim_replay_commit (raft-apply-decoupling task 7.1; Req 10.3): re-invoke
* node_idx's OWN registered on_commit_advanced callback with its CURRENT
* commit_index — simulating a replay or retry of an already-processed commit
* notification. Bypasses the raft library's own fire-once-per-strict-advance
* contract (raft_advance_commit never re-fires on a held index) so the callback's
* OWN idempotency can be exercised directly, independent of whether the library
* would ever naturally re-invoke it. Works for clusters from either
* raft_sim_init or raft_sim_conformance_init, since both wire on_commit_advanced
* through node->cbs. No-op if node_idx is out of range or the node has no
* registered callback.
*/
void raft_sim_replay_commit(raft_sim_cluster_t *c, int node_idx);
/*
* raft_sim_restart_node: model a process restart of node_idx (Req 8.3).
*

92
src/lib/raft/raft_sim.c
View file

@ -37,6 +37,11 @@ static void sim_noop_start_election_after_delay(void *ctx, uint32_t delay_ms)
/* ---------- wired callbacks ---------- */
/* Forward declaration: sim_conf_decode_value is defined further below (conformance
* harness adapter section) but sim_persist_entry's RAFT_SIM_BREAK_APPLY_BEFORE_COMMIT
* fault branch (raft-apply-decoupling task 7.1) needs it earlier in the file. */
static uint64_t sim_conf_decode_value(const raft_sim_entry_t *slot);
/*
* sim_send_vote_request: buffer a pending RPC into the cluster queue.
*
@ -125,6 +130,15 @@ static int sim_persist_entry(void *ctx, uint64_t index, uint64_t term,
memcpy(slot->bytes, entry, n);
slot->len = n;
/* Deliberately-broken-build fault switch (raft-apply-decoupling task 7.1): when
* RAFT_SIM_BREAK_APPLY_BEFORE_COMMIT is set, eagerly decode and write this
* entry's value into applied[] right here at persist time — BEFORE it has ever
* committed — emulating an apply-before-commit regression (the defect class
* raft-apply-decoupling fixes). Purely additive — DEFAULT OFF, so legacy and
* conformance runs that never set the flag are byte-identical to before. */
if (c && (c->fault_inject & RAFT_SIM_BREAK_APPLY_BEFORE_COMMIT))
node->applied[index - 1] = sim_conf_decode_value(slot);
if ((int)index > node->log_count)
node->log_count = (int)index;
@ -314,12 +328,29 @@ static uint64_t sim_conf_decode_value(const raft_sim_entry_t *slot)
static void sim_conf_on_commit_advanced(void *ctx, uint64_t commit_index)
{
raft_sim_node_t *node = (raft_sim_node_t *)ctx;
raft_sim_cluster_t *c = (raft_sim_cluster_t *)node->ctx;
/* Deliberately-broken-build fault switch (raft-apply-decoupling task 7.1): when
* RAFT_SIM_BREAK_REAPPLY_GUARD is set, widen the apply range to the FULL
* committed prefix (1..commit_index) on EVERY call instead of only the
* newly-committed suffix (prev+1..commit_index) — emulating a regression where
* a retried/duplicate commit notification re-applies entries that were already
* applied. Purely additive — DEFAULT OFF, so a normal call (including a forced
* raft_sim_replay_commit retry) remains exactly as before: a no-op when
* commit_index has not strictly advanced. */
int reapply_guard_broken = c && (c->fault_inject & RAFT_SIM_BREAK_REAPPLY_GUARD);
uint64_t prev = node->commit_index;
if (commit_index > prev) {
for (uint64_t k = prev + 1; k <= commit_index; k++) {
if (k >= 1 && k <= (uint64_t)node->log_count && k <= RAFT_SIM_MAX_LOG)
if (commit_index > prev || reapply_guard_broken) {
uint64_t from = reapply_guard_broken ? 1 : prev + 1;
for (uint64_t k = from; k <= commit_index; k++) {
if (k >= 1 && k <= (uint64_t)node->log_count && k <= RAFT_SIM_MAX_LOG) {
node->applied[k - 1] = sim_conf_decode_value(&node->log[k - 1]);
/* Reaction-fire mirror (Req 10.3): counts genuine applies of
* committed index k, so raft_sim_check_idempotent_reapply can
* assert it never exceeds 1. */
node->apply_reaction_count[k - 1]++;
}
}
}
@ -797,6 +828,22 @@ void raft_sim_advance_commit(raft_sim_cluster_t *c, int node_idx)
(void)raft_advance_commit(&c->nodes[node_idx].state);
}
/*
* raft_sim_replay_commit (raft-apply-decoupling task 7.1; Req 10.3): re-invoke
* node_idx's own registered on_commit_advanced callback with its CURRENT
* commit_index, simulating a replay/retry of an already-processed commit
* notification. See raft.h for the full contract.
*/
void raft_sim_replay_commit(raft_sim_cluster_t *c, int node_idx)
{
if (!c || node_idx < 0 || node_idx >= c->n)
return;
raft_sim_node_t *node = &c->nodes[node_idx];
if (node->cbs.on_commit_advanced)
node->cbs.on_commit_advanced(node, node->state.commit_index);
}
/* Two log entries are identical iff their term, length, and payload bytes
* (over the recorded length) all match. */
static int sim_entry_identical(const raft_sim_entry_t *a,
@ -929,6 +976,45 @@ int raft_sim_check_state_machine_safety(const raft_sim_cluster_t *c)
return 1; /* holds */
}
int raft_sim_check_apply_after_commit(const raft_sim_cluster_t *c)
{
/* Additive check (raft-apply-decoupling task 7.1, Req 10.1) — NOT one of the
* four raft.tla invariants and NOT evaluated by raft_sim_check_all; see raft.h.
* applied[k-1] != 0 is treated as "index k has been applied" (the same
* zero-means-absent convention this file already uses for log-entry terms);
* every value this harness ever applies is non-zero in practice. */
for (int i = 0; i < c->n; i++) {
const raft_sim_node_t *node = &c->nodes[i];
int limit = node->log_count;
if (limit > RAFT_SIM_MAX_LOG)
limit = RAFT_SIM_MAX_LOG;
for (int k = 1; k <= limit; k++) {
if (node->applied[k - 1] != 0 && (uint64_t)k > node->commit_index)
return 0; /* applied ahead of commit — Req 10.1 violated */
}
}
return 1; /* holds */
}
int raft_sim_check_idempotent_reapply(const raft_sim_cluster_t *c)
{
/* Additive check (raft-apply-decoupling task 7.1, Req 10.3) — NOT one of the
* four raft.tla invariants and NOT evaluated by raft_sim_check_all; see raft.h. */
for (int i = 0; i < c->n; i++) {
const raft_sim_node_t *node = &c->nodes[i];
int limit = node->log_count;
if (limit > RAFT_SIM_MAX_LOG)
limit = RAFT_SIM_MAX_LOG;
for (int k = 1; k <= limit; k++) {
if (node->apply_reaction_count[k - 1] > 1)
return 0; /* re-applied — Req 10.3 violated */
}
}
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