wdgzyjx/myxce
1
0
Fork 0
forked from lei.chen/myxce
Code Pull requests Activity

feat(raft-sim-conformance): optional TLC-consumable trace export, default-off (task 8.1)

Browse source
This commit is contained in:
Rongsong Shen 2026-06-24 16:49:36 +00:00
parent ffeb7c2cf5
commit 95629797f8
4 changed files with 242 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
.kiro/specs/raft-sim-conformance/tasks.md
View file

@ -201,7 +201,7 @@
## 8. Optional TLC-consumable trace export
- [ ]* 8.1 TLC-consumable trace export (deferred; off by default)
- [x]* 8.1 TLC-consumable trace export (deferred; off by default)
- Implement `raft_sim_export_trace` gated by `RAFT_SIM_EXPORT`: per step, emit the action + tracked `raft.tla` variables (`messages` summary, per-node `currentTerm`/`state`/`log`/`commitIndex`) named per `raft/raft.tla`, in a stable line-oriented format; off by default
- Observable completion: with `RAFT_SIM_EXPORT` set, a run emits a stable, spec-named record stream; default runs emit nothing extra
- _Requirements: 8.1, 8.2, 8.3_

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

@ -923,6 +923,23 @@ void raft_sim_trace_record(raft_sim_cluster_t *c, raft_sim_action_t action);
void raft_sim_dump_trace(const raft_sim_cluster_t *c, FILE *fp,
raft_sim_invariant_t failing);
/*
* raft_sim_export_trace: optional TLC-consumable trace export (task 8.1; Req 8.1,
* 8.2, 8.3). Emits a STABLE, line-oriented, machine-readable record of the
* harness's tracked raft.tla variables to `fp`: a header line (seed, n), the
* ordered action trace (each action named per raft.tla's Next disjuncts), and the
* resulting tracked variables — per node `currentTerm`, `state` (Follower/
* Candidate/Leader), `log` (the (term, value) sequence), `commitIndex`, plus a
* `messages` bag summary. Names match raft/raft.tla (R8.2) so the export maps to
* spec actions/variables without re-interpretation.
*
* Gated OFF by default (R8.3): a no-op (emits NOTHING) unless the RAFT_SIM_EXPORT
* environment variable is set — mirroring the RAFT_SIM_VERBOSE quiet-on-success
* idiom. The standard CI conformance run never sets it, so it incurs no export
* overhead. Output is deterministic/stable (no addresses, no wall-clock).
*/
void raft_sim_export_trace(const raft_sim_cluster_t *c, FILE *fp);
/*
* raft_sim_advance_commit: drive raft_advance_commit on node_idx (task 6.1).
*

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

@ -1015,6 +1015,137 @@ void raft_sim_dump_trace(const raft_sim_cluster_t *c, FILE *fp,
}
}
/* ---------- optional TLC-consumable trace export (task 8.1) ---------- */
/*
* sim_tla_action_name: map a harness action kind to the corresponding raft.tla
* `Next` disjunct name (R8.2), so the export reads in the spec's own vocabulary
* (raft.tla:454). Distinct from raft_sim_action_kind_name (kebab-case, human dump):
* this is the PascalCase spec-action name a maintainer maps directly to raft.tla.
*/
static const char *sim_tla_action_name(raft_sim_action_kind_t kind)
{
switch (kind) {
case RAFT_SIM_ACT_RESTART: return "Restart"; /* raft.tla:166 */
case RAFT_SIM_ACT_TIMEOUT: return "Timeout"; /* raft.tla:178 */
case RAFT_SIM_ACT_REQUEST_VOTE: return "RequestVote"; /* raft.tla:190 */
case RAFT_SIM_ACT_BECOME_LEADER: return "BecomeLeader"; /* raft.tla:229 */
case RAFT_SIM_ACT_CLIENT_REQUEST: return "ClientRequest"; /* raft.tla:246 */
case RAFT_SIM_ACT_APPEND_ENTRIES: return "AppendEntries"; /* raft.tla:218 */
case RAFT_SIM_ACT_ADVANCE_COMMIT: return "AdvanceCommitIndex"; /* raft.tla:259 */
case RAFT_SIM_ACT_RECEIVE: return "Receive"; /* raft.tla:421 */
case RAFT_SIM_ACT_DUPLICATE_MESSAGE: return "DuplicateMessage"; /* raft.tla:443 */
case RAFT_SIM_ACT_DROP_MESSAGE: return "DropMessage"; /* raft.tla:448 */
}
return "Unknown";
}
/*
* sim_tla_state_name: map the library role enum to the raft.tla `state` value name
* (Follower/Candidate/Leader, raft.tla:17/144) so the per-node export uses the spec
* name for `state[i]` directly.
*/
static const char *sim_tla_state_name(raft_role_t role)
{
switch (role) {
case RAFT_FOLLOWER: return "Follower";
case RAFT_CANDIDATE: return "Candidate";
case RAFT_LEADER: return "Leader";
}
return "Unknown";
}
/*
* sim_tla_msg_kind_name: map a bag message kind to the raft.tla message `mtype`
* (RequestVoteRequest/RequestVoteResponse/AppendEntriesRequest/AppendEntriesResponse,
* raft.tla:23-24) for the `messages` bag summary.
*/
static const char *sim_tla_msg_kind_name(raft_sim_msg_kind_t kind)
{
switch (kind) {
case RAFT_SIM_MSG_VOTE_REQ: return "RequestVoteRequest";
case RAFT_SIM_MSG_VOTE_RSP: return "RequestVoteResponse";
case RAFT_SIM_MSG_AE_REQ: return "AppendEntriesRequest";
case RAFT_SIM_MSG_AE_RSP: return "AppendEntriesResponse";
}
return "Unknown";
}
/*
* raft_sim_export_trace: STABLE, line-oriented, machine-readable export of the
* harness's tracked raft.tla variables (R8.1) using raft.tla-consistent names (R8.2),
* gated OFF by default behind RAFT_SIM_EXPORT (R8.3 — mirrors the RAFT_SIM_VERBOSE
* idiom in raft_sim_dump_trace). Documented format (one record per line; fields are
* `key=value`; deterministic — no addresses, no wall-clock):
*
* trace-export seed=<u64> n=<int> steps=<trace_len>
* action <i> name=<RaftTlaActionName> actor=<int> msg_index=<int> term=<u64> index=<u64>
* ... one per recorded c->trace[] step, in order ...
* node <i> currentTerm=<u64> state=<Follower|Candidate|Leader> commitIndex=<u64> \
* log=[(<term>,<value>);...]
* ... one per node ...
* messages count=<int> [<i>]=<MsgType>{src=..,dst=..,term=..} ...
*
* The action lines ARE the per-step sequence (R8.1's "per step"); a deterministic
* replay from (seed, n, steps) reconstructs the per-step intermediate state, while the
* node/messages lines pin the resulting tracked variables. `log` decodes each entry's
* client value with the same little-endian decode applied[] uses, so the (term, value)
* sequence matches raft.tla `log[i]`.
*/
void raft_sim_export_trace(const raft_sim_cluster_t *c, FILE *fp)
{
/* Default-OFF gate (R8.3): emit NOTHING unless explicitly enabled. */
if (getenv("RAFT_SIM_EXPORT") == NULL)
return;
/* Header: run key + step count (R8.1). */
fprintf(fp, "trace-export seed=%llu n=%d steps=%d\n",
(unsigned long long)c->seed, c->n, c->trace_len);
/* Ordered action trace — each named per raft.tla's Next disjuncts (R8.2). */
for (int i = 0; i < c->trace_len; i++) {
const raft_sim_action_t *a = &c->trace[i];
fprintf(fp,
"action %d name=%s actor=%d msg_index=%d term=%llu index=%llu\n",
i, sim_tla_action_name(a->kind), a->actor, a->msg_index,
(unsigned long long)a->term, (unsigned long long)a->index);
}
/* Per-node resulting tracked variables: currentTerm, state, commitIndex, log
* (the (term, value) sequence) — raft.tla variable names (R8.1, R8.2). */
for (int i = 0; i < c->n; i++) {
const raft_sim_node_t *node = &c->nodes[i];
raft_snapshot_t snap;
raft_snapshot(&node->state, &snap);
fprintf(fp, "node %d currentTerm=%llu state=%s commitIndex=%llu log=[",
i, (unsigned long long)snap.term,
sim_tla_state_name(snap.role),
(unsigned long long)node->commit_index);
for (int k = 1; k <= node->log_count; k++) {
const raft_sim_entry_t *slot = &node->log[k - 1];
uint64_t value = sim_conf_decode_value(slot);
fprintf(fp, "%s(%llu,%llu)", (k > 1) ? ";" : "",
(unsigned long long)slot->term,
(unsigned long long)value);
}
fprintf(fp, "]\n");
}
/* `messages` bag summary: count + per-member (type, src, dst, term). Mirrors
* raft.tla `messages` (the in-flight RPC bag). */
fprintf(fp, "messages count=%d", c->bag_count);
for (int i = 0; i < c->bag_count; i++) {
const raft_sim_msg_t *m = &c->bag[i];
fprintf(fp, " [%d]=%s{src=%d,dst=%d,term=%llu}",
i, sim_tla_msg_kind_name(m->kind), m->src, m->dst,
(unsigned long long)m->term);
}
fprintf(fp, "\n");
}
int raft_sim_restart_node(raft_sim_cluster_t *c, int node_idx)
{
if (node_idx < 0 || node_idx >= c->n)

93
src/lib/testsuite/test_raft.c
View file

@ -5362,6 +5362,98 @@ static void test_sim_4_1_trace_record_and_dump(void)
setenv("RAFT_SIM_VERBOSE", saved_copy, 1);
}
/*
* test_sim_8_1_export_trace_named_and_gated (raft-sim-conformance task 8.1;
* Req 8.1, 8.2, 8.3)
*
* raft_sim_export_trace emits a STABLE, line-oriented, machine-readable record of
* the harness's tracked raft.tla variables, gated OFF by default via the
* RAFT_SIM_EXPORT environment variable (mirroring the RAFT_SIM_VERBOSE idiom):
* - Export ON (RAFT_SIM_EXPORT set): a post-run cluster's export CONTAINS the
* spec-named tokens (currentTerm, state, log, commitIndex, messages — R8.2),
* the seed/n header, and at least one action name from the recorded trace
* (R8.1). Two exports of the same post-run state are byte-identical (stable).
* - Default OFF (RAFT_SIM_EXPORT unset): the export emits NOTHING (R8.3).
* The env var is saved and restored around the test so the rest of the suite is
* unperturbed.
*/
static void test_sim_8_1_export_trace_named_and_gated(void)
{
/* Save + clear the gate so we control it deterministically. */
char *saved_export = getenv("RAFT_SIM_EXPORT");
char saved_copy[256];
int had_export = (saved_export != NULL);
if (had_export) {
strncpy(saved_copy, saved_export, sizeof(saved_copy) - 1);
saved_copy[sizeof(saved_copy) - 1] = '\0';
}
/* Drive a short deterministic run so trace[] holds actions and nodes carry
* observable state (term/log/commit). Seed 3 is the one the 4.2 test proves
* completes a clean run on the correct library. */
raft_sim_cluster_t c;
memset(&c, 0, sizeof(c));
TEST_ASSERT_EQUAL_INT(0, raft_sim_conformance_init(&c, 3, 2000, 3ULL));
for (int step = 0; step < 80; step++) {
int rc = raft_sim_step(&c);
TEST_ASSERT_TRUE(rc >= 0);
}
TEST_ASSERT_TRUE(c.trace_len > 0); /* the run recorded actions to export */
/* ---- Export ON (R8.1, R8.2) ---- */
setenv("RAFT_SIM_EXPORT", "1", 1);
char buf[8192];
memset(buf, 0, sizeof(buf));
FILE *fp = fmemopen(buf, sizeof(buf), "w");
TEST_ASSERT_NOT_NULL(fp);
raft_sim_export_trace(&c, fp);
fclose(fp);
TEST_ASSERT_TRUE(strlen(buf) > 0);
/* raft.tla-named tracked variables (R8.2). */
TEST_ASSERT_NOT_NULL(strstr(buf, "currentTerm"));
TEST_ASSERT_NOT_NULL(strstr(buf, "state"));
TEST_ASSERT_NOT_NULL(strstr(buf, "log"));
TEST_ASSERT_NOT_NULL(strstr(buf, "commitIndex"));
TEST_ASSERT_NOT_NULL(strstr(buf, "messages"));
/* seed/n header (R8.1). */
{
char seedtok[32];
snprintf(seedtok, sizeof(seedtok), "%llu", (unsigned long long)c.seed);
TEST_ASSERT_NOT_NULL(strstr(buf, seedtok));
TEST_ASSERT_NOT_NULL(strstr(buf, "seed"));
TEST_ASSERT_NOT_NULL(strstr(buf, "n="));
}
/* At least one raft.tla Next action name appears (R8.1/R8.2). The scheduler
* always drives Timeout, so it is reliably present. */
TEST_ASSERT_NOT_NULL(strstr(buf, "Timeout"));
/* Stability: a second export of the same post-run state is byte-identical. */
char buf2[8192];
memset(buf2, 0, sizeof(buf2));
FILE *fp2 = fmemopen(buf2, sizeof(buf2), "w");
TEST_ASSERT_NOT_NULL(fp2);
raft_sim_export_trace(&c, fp2);
fclose(fp2);
TEST_ASSERT_EQUAL_INT(0, strcmp(buf, buf2)); /* deterministic / stable */
/* ---- Default OFF (R8.3): gate unset => emit NOTHING ---- */
unsetenv("RAFT_SIM_EXPORT");
char qbuf[256];
memset(qbuf, 0, sizeof(qbuf));
FILE *qfp = fmemopen(qbuf, sizeof(qbuf), "w");
TEST_ASSERT_NOT_NULL(qfp);
raft_sim_export_trace(&c, qfp);
fclose(qfp);
TEST_ASSERT_EQUAL_INT(0, (int)strlen(qbuf)); /* silent unless explicitly enabled */
if (had_export)
setenv("RAFT_SIM_EXPORT", saved_copy, 1);
else
unsetenv("RAFT_SIM_EXPORT");
}
/* ---------- Group A: Basic Election Correctness (task 5.1) ---------- */
/*
@ -9020,6 +9112,7 @@ void test_raft(void)
RUN_TEST(test_sim_2_2_drop_duplicate_preserve_node_state);
RUN_TEST(test_sim_2_2_reorder_prng_deterministic);
RUN_TEST(test_sim_4_1_trace_record_and_dump);
RUN_TEST(test_sim_8_1_export_trace_named_and_gated);
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);