wdgzyjx/myxce
1
0
Fork 0
forked from lei.chen/myxce
Code Pull requests Activity
myxce/.kiro/specs/raft-sim-conformance/design.md

32 KiB
Raw Blame History

Design Document

Overview

Purpose: This feature turns src/lib/raft/raft_sim.c (today an election-only RPC router) into an in-process TLA+ conformance harness for the XCE Raft core. It drives N library instances synchronously through transitions equivalent to the raft.tla Next actions (raft.tla:454) and asserts the four Raft safety invariants after every step. It delivers an independent regression oracle for the consensus core — the "use the verified spec to help" payoff — that would have caught bug-851 (the silent committed-prefix divergence) before it shipped.

Users: Raft library maintainers (verifying raft.c), the raft-log-replication and raft-commit-safety authors (whose entry points this harness exercises), and CI (which runs the harness as a first-class library test target).

Impact: Replaces ad-hoc election-only simulation with a complete in-process model of the raft.tla state space: a shared message bag mirroring messages, per-node state mirroring serverVars/logVars/leaderVars, an action scheduler, four invariant checkers, and a failure-trace recorder. The protocol implementation is unchanged — the harness drives it only through the published entry points and callbacks from the two upstream specs; the harness itself is the in-memory adapter (it implements the WAL/ transport callbacks against in-memory structures).

Goals

  • A deterministic, seedable driver that mirrors the raft.tla messages bag and the per-node variables this harness tracks, driving the library entry points only.
  • Per-step assertion of all four safety invariants (Election Safety, Log Matching, Leader Completeness, State Machine Safety) computed purely from observable node state.
  • Targeted adversarial scenarios (partition/heal, restart, drop/dup/reorder, Figure-8, bug-851 G5 term-reuse) plus randomized seed sweeps.
  • A replayable failure trace (seed + ordered action list) and a CI-runnable target.
  • A deliberately-broken-build negative test proving the oracle catches a bug-851-class divergence and passes on the correct build.
  • Optionally, a TLC-consumable trace export.

Non-Goals

  • No protocol semantics. logOk, conflict truncation, the current-term commit rule, (lastLogTerm, lastLogIndex) freshness, and UpdateTerm adoption live in raft.c (owned by raft-log-replication / raft-commit-safety). The harness drives and checks them; it never re-implements them.
  • No live cluster / controller integration. The /xce-deploy-ha chaotic-failover regression, controller WAL/repl/recovery/commit-barrier internals, config markers, and the upgrade snapshot are ha-term-safety.
  • No changes to raft/raft.tla and no TLC model-checker harness for the spec (only an optional export the maintainer can feed to TLC manually).
  • No async I/O, threads, or sockets. The harness is synchronous and deterministic by construction.

Boundary Commitments

This Spec Owns

  • src/lib/raft/raft_sim.c — the harness body: the shared message bag, per-node in-memory log + commit + applied state, the in-memory adapter callbacks, the seeded action scheduler, the four invariant checkers, the trace recorder, the scenario generators, and the deliberately-broken-build fault switch wiring (test-only).
  • The harness public surface in raft.h's XCE_TESTING section: new sim types (message-bag entry, per-node log array, action record) and the new raft_sim_* driver functions. These extend — never alter — the protocol declarations.
  • The conformance test entry point + scenarios in src/lib/testsuite/test_raft.c (XCE_TESTING-gated), including the negative (broken-build) test.

Out of Boundary

  • The protocol entry points and callback semantics (raft_log_append, raft_send_append_entries, raft_on_append_entries_request/reply, raft_advance_commit, the vote path, on_persist_entry, on_get_entry_term, on_send_append_entries, on_truncate_from, on_commit_advanced) — owned by raft-log-replication / raft-commit-safety. This spec consumes them verbatim.
  • Any raft.c change to protocol logic. The harness must not need one; if it does, that is an upstream-spec gap, not a harness change.
  • The controller-side adapters, WAL byte layout, repl transport, recovery, commit barrier, config markers, snapshot — ha-term-safety.
  • raft/raft.tla itself and any TLC tooling.

Allowed Dependencies

  • The raft-log-replication shared callback contract verbatim: on_persist_entry, on_get_entry_term, on_send_append_entries, on_truncate_from; the 1-based index = WAL LSN identity; the term 0 = absent convention; per-peer next_index[]/ match_index[]; entry points raft_log_append, raft_send_append_entries, raft_on_append_entries_request, raft_on_append_entries_reply, raft_append_result_t.
  • The raft-commit-safety additions: raft_advance_commit (current-term-gated AdvanceCommitIndex), on_commit_advanced, and the (lastLogTerm, lastLogIndex) vote freshness already enforced inside the vote handlers.
  • The implemented election core (raft-library): raft_init, raft_start_election, raft_on_vote_request/reply, raft_on_election_timeout, PreVote, raft_snapshot.
  • Only errno.h, stdint.h, string.h, stdio.h, unity/unity.h (test) — the simulator stays free-standing, like the rest of the library, and is XCE_TESTING-gated.

Revalidation Triggers

Re-check this design if any upstream changes:

  • The signature/semantics of any of the four log-replication callbacks or on_commit_advanced.
  • The signature/return semantics of raft_log_append, raft_send_append_entries, raft_on_append_entries_request, raft_on_append_entries_reply, raft_advance_commit, or raft_append_result_t.
  • The 1-based-index ↔ WAL-LSN identity or the term 0 = absent convention.
  • The placement of UpdateTerm / DropStaleResponse inside the handlers (the harness relies on the handlers performing these, not the harness).

Architecture

Existing Architecture Analysis

raft_sim.c already establishes the harness idiom this design extends:

  • A raft_sim_cluster_t owning nodes[RAFT_SIM_MAX_NODES], a pending[] RPC queue, and cluster-level counters.
  • Each raft_sim_node_t carries raft_state_t state, a raft_callbacks_t cbs wired to sim routing functions, a back-pointer ctx to the cluster, an idx, a partition flag, and a trace_buf.
  • Callbacks cast ctx back to raft_sim_node_t*, reaching the cluster via node->ctx.
  • Routing is synchronous: raft_sim_deliver_pending drains the queue, calling raft_on_vote_request on the destination and routing the reply back.

This design keeps that idiom and adds: a richer message bag (vote and AppendEntries, requests and responses), an in-memory log + commit + applied state per node, the four new adapter callbacks, a seeded action scheduler, invariant checkers, and a trace recorder. No new file is introduced; the existing module is extended (consistent with how raft-log-replication extends raft_sim.c).

TLA+ variable → harness state mapping

The harness mirrors exactly the raft.tla variables it needs to drive actions and check invariants. The protocol-internal portions of serverVars/leaderVars (currentTerm, votedFor, state, nextIndex, matchIndex) live inside each raft_state_t and are read through raft_snapshot and the library's own fields — the harness does not duplicate them.

raft.tla variable Harness home Read/owned
messages (bag of in-flight RPCs) cluster.bag[] (requests + responses) harness-owned
currentTerm[i], state[i], votedFor[i] node.state (raft_state_t) library-owned, read via snapshot/fields
log[i] (sequence of (index, term, value)) node.log[] in-memory array harness-owned (the adapter)
commitIndex[i] node.commit_index harness-owned, advanced via raft_advance_commit + on_commit_advanced
nextIndex[i][j], matchIndex[i][j] node.state.next_index[]/match_index[] library-owned
applied state machine (for SM Safety) node.applied[] (value per committed index) harness-owned
allLogs (history of every log) cluster.all_logs snapshot used by checkers harness-owned

Component / data-flow map

flowchart TB
    subgraph SCHED["Action Scheduler (raft_sim.c) — seeded PRNG"]
        PICK["pick action ~ raft.tla Next (454)"]
        REC["record action -> trace buffer (R1.4)"]
    end
    subgraph NODES["N library instances (raft.c — UNCHANGED)"]
        ST["raft_state_t (term, role, votedFor, next/match)"]
        EP["entry points: start_election, on_vote_*,<br/>log_append, send_append_entries,<br/>on_append_entries_*, advance_commit"]
    end
    subgraph ADAPT["In-memory adapter callbacks (raft_sim.c = the adapter)"]
        A1["on_persist_entry -> node.log[]"]
        A2["on_get_entry_term -> node.log[idx].term &#124; 0"]
        A3["on_send_append_entries -> bag.push(AE req)"]
        A4["on_truncate_from -> node.log truncate"]
        A5["on_commit_advanced -> node.commit_index + apply()"]
        A6["on_send_vote_request -> bag.push(vote req)"]
    end
    subgraph BAG["Message bag (cluster.bag[]) — mirrors raft.tla messages"]
        B["vote/AE requests + responses,<br/>Drop/Duplicate/Reorder live here"]
    end
    subgraph CHK["Invariant checkers (after every step, R3)"]
        I1["Election Safety"]
        I2["Log Matching"]
        I3["Leader Completeness"]
        I4["State Machine Safety"]
    end
    PICK --> REC --> EP
    EP --> A1 & A2 & A3 & A4 & A5 & A6
    A3 & A6 --> BAG
    BAG -->|Receive/Deliver| EP
    EP --> CHK
    CHK -->|violation| FAIL["halt + dump seed & trace (R5)"]

Architecture integration

  • Pattern: model-based test harness over a pure state machine. The library is the system-under-test (Ports-and-Adapters: the harness implements all callback ports against in-memory structures). The scheduler is a seeded interleaving engine over the raft.tla action set; the checkers are pure observers.
  • Domain boundary: protocol decisions stay in raft.c; driving (which action, which message) and checking (the four invariants) stay in the harness.
  • Preserved patterns: ctx-back-pointer callbacks, synchronous routing, XCE_TESTING gating, per-node trace buffers, the raft_sim_* naming.
  • Steering compliance: src/lib/CLAUDE.md (free-standing gnu17, tests in testsuite/), ha-async-io.md (no blocking — and here, no async at all), testing.md (TDD: checkers/scenarios written before they pass), "controller never self-terminates" (the harness abort()s a test on violation, never the library).

Technology Stack

Layer Choice Role Notes
Harness core C (gnu17), string.h/stdint.h/stdio.h message bag, scheduler, checkers, trace XCE_TESTING-gated; free-standing
PRNG small inlined deterministic generator (e.g. SplitMix64/xorshift) seeded by a uint64_t all nondeterministic choices no libc rand() (not reproducible across platforms)
Adapter in-memory node.log[], commit_index, applied[] implements the 6 callbacks the harness IS the WAL/transport adapter
Test runner Unity (unity/unity.h) in test_raft.c scenario + seed-sweep + negative test built by src/lib/meson.build test target
Fault switch compile-time macro (e.g. RAFT_SIM_BREAK_*) in the test build only negative test never set in default CI run

File Structure Plan

Modified Files

  • src/lib/raft/raft.h (XCE_TESTING section only) — extend the sim types: a unified message-bag entry (raft_sim_msg_t: kind = vote-req/vote-rsp/ae-req/ae-rsp, src, dst, and a union of payload fields incl. term, prev_log_index/term, leader_commit, entry bytes + entry_term, match_index, granted/success); a per-node in-memory log entry (raft_sim_log_entry_t { uint64_t term; uint64_t value; }); an action record (raft_sim_action_t: kind + actor + target/message identity); extend raft_sim_node_t with log[], log_len, commit_index, applied[]; extend raft_sim_cluster_t with the bag, the PRNG state, the trace buffer, and the seed; declare the new raft_sim_* driver/scenario/check functions. No protocol declaration is changed.
  • src/lib/raft/raft_sim.c — the harness implementation (sections below): adapter callbacks, bag operations (push/deliver/drop/duplicate/reorder), the seeded action scheduler (raft_sim_step / raft_sim_run), the four invariant checkers (raft_sim_check_* + raft_sim_check_all), the trace recorder + dumper, the targeted scenario drivers, and the fault-switch hooks (compile-time-gated).
  • src/lib/testsuite/test_raft.c — the conformance test cases: targeted scenarios, the randomized M-seed sweep, the replay-reproduction test, and the negative (broken-build) test.

Directory Structure (unchanged)

src/lib/raft/
├── raft.h          # + sim message bag, in-memory log, action record, driver decls (XCE_TESTING)
├── raft.c          # UNCHANGED by this spec (protocol owned upstream)
└── raft_sim.c      # + bag, scheduler, 4 invariant checkers, trace, scenarios, fault hooks
src/lib/testsuite/
└── test_raft.c     # + conformance scenarios, M-seed sweep, replay test, negative test

Single-responsibility kept: raft.c = pure protocol (untouched), raft_sim.c = deterministic harness + in-memory adapter + checkers, test_raft.c = assertions and the CI batch.

System Flows

One scheduler step (the Next interleaving)

sequenceDiagram
    participant S as Scheduler (seeded PRNG)
    participant L as Library node (raft.c)
    participant A as Adapter cb (raft_sim.c)
    participant B as Message bag
    participant C as Checkers
    S->>S: action = pick(Next set) from PRNG
    S->>S: record(action) into trace (R1.4)
    alt node-local (Timeout / RequestVote / BecomeLeader / ClientRequest)
        S->>L: call entry point (start_election / log_append / ...)
        L->>A: on_persist_entry / on_send_* (drives bag/log)
        A->>B: push request(s)
    else AppendEntries (leader replicate)
        S->>L: raft_send_append_entries(peer, leader_commit)
        L->>A: on_send_append_entries -> bag.push(AE req)
    else AdvanceCommitIndex
        S->>L: raft_advance_commit()
        L->>A: on_commit_advanced -> commit_index advanced, apply()
    else Receive (deliver one bag message)
        S->>B: pop selected message
        S->>L: route to handler (on_vote_request / on_append_entries_request / *_reply)
        L->>A: UpdateTerm/persist/truncate/append + reply push
    else DropMessage / DuplicateMessage
        S->>B: discard / re-enqueue (no node mutation) (R2.5)
    else Restart
        S->>L: raft_init preserving persisted term/votedFor + restore log_len (R2.1)
    end
    S->>C: raft_sim_check_all() (R3)
    alt any invariant violated
        C-->>S: fail -> dump seed + trace + invariant (R5), then halt
    else ok
        C-->>S: continue
    end

Flow-level decisions:

  • The library performs the protocol; the harness performs the interleaving. UpdateTerm and DropStaleResponse happen inside the handlers (R2.4); the harness never pre-filters by term — that would mask the very bugs it must catch.
  • Commit is library-gated. The harness calls raft_advance_commit; the current-term Figure-8 rule is enforced by raft.c. The harness only applies whatever the library reports committed via on_commit_advanced, then checks State Machine Safety.
  • Faults are bag-only. Drop/Duplicate/Reorder mutate cluster.bag[] exclusively (R2.5), mirroring raft.tla:443/448 (UNCHANGED of all non-message vars).
  • Restart preserves persistence. The harness keeps node.log[], the recovered log_len, and the last-persisted (term, votedFor) across a raft_init, matching raft.tla Restart (keeps currentTerm, votedFor, log; resets volatile state).

Invariant checker construction (observable-state-only)

flowchart LR
    subgraph IN["inputs: per-node observable state"]
        R["roles+terms (raft_snapshot)"]
        LG["node.log[] (index, term, value)"]
        CM["node.commit_index"]
        AP["node.applied[]"]
    end
    R --> ES["Election Safety: &#124;{i: role==LEADER, term==t}&#124; <= 1, all t (R3.1)"]
    LG --> LM["Log Matching: pairwise, shared (idx,term) => identical prefix (R3.2)"]
    LG --> LC["Leader Completeness: committed entry in every higher-term leader log (R3.3)"]
    CM --> LC
    AP --> SM["State Machine Safety: applied[i][k] == applied[j][k] for all k (R3.4)"]

Requirements Traceability

Requirement Summary Design elements raft.tla anchor
1.1–1.6 Deterministic seedable driver seeded PRNG; cluster.bag[]; per-node log[]/commit_index/applied[]; trace buffer; no threads/sockets/clock; deterministic replay messages, serverVars, logVars
2.1–2.6 Drive Next-equivalent actions via library entry points scheduler step dispatch; raft_send_append_entries; raft_advance_commit; handler routing (UpdateTerm/DropStale inside lib); bag-only Drop/Dup; entry-points-only rule Next (454), Restart/Timeout/RequestVote/BecomeLeader/ClientRequest/AppendEntries/AdvanceCommitIndex/Receive/Duplicate/Drop
3.1–3.6 Per-step four-invariant assertion raft_sim_check_election_safety/log_matching/leader_completeness/state_machine_safety; raft_sim_check_all; halt-on-fail; observable-state-only Election Safety / Log Matching / Leader Completeness / State Machine Safety
4.1–4.5 Targeted scenarios raft_sim_scenario_partition_heal/restart_churn/drop_dup_reorder/figure8/stale_rejoin partition / Restart / message faults / Figure-8 / G5
5.1–5.4 Failure-trace capture + replay trace recorder; raft_sim_dump_trace (seed + ordered actions); replay from seed; quiet-on-success (verification)
6.1–6.4 CI-runnable target test_raft.c conformance entry; M-seed batch + scenarios; ASAN/UBSAN clean; bounded steps/seeds (verification)
7.1–7.4 Deliberately-broken-build negative test compile-time RAFT_SIM_BREAK_* fault switch (test build only); both-direction assertion bug-851 G1/G3 mechanism
8.1–8.3 Optional TLC-consumable trace export stable machine-readable record named per raft.tla; off by default raft.tla actions/vars

Components and Interfaces

Component Layer Intent Req coverage Key dependencies Contract
Message bag Harness Mirror messages; carry vote/AE req+rsp 1, 2 raft_sim_msg_t State
In-memory adapter callbacks Harness Implement the 6 ports against node.log[]/commit 1, 2 upstream callback contract (P0) Service
Action scheduler Harness Seeded interleaving over the Next set 1, 2 PRNG, entry points (P0) Service
Invariant checkers Harness Assert the four safety properties 3 observable node state Service
Trace recorder Harness Record + dump replayable action trace 1, 5 scheduler Service
Scenario drivers Harness Targeted adversarial cases 4 scheduler, bag Service
Fault switch Test build Deliberately-broken build 7 compile-time macro Service
Conformance test Test suite CI batch + negative test 6, 7 all of the above Test

In-memory adapter callbacks (the harness as adapter)

The harness implements the upstream callbacks against per-node in-memory state, exactly as the raft-log-replication design anticipates ("bytes live in the adapter (WAL) / simulator (in-memory array)"). Signatures are consumed verbatim from upstream; behavior:

Callback Harness behavior
on_persist_entry(ctx, index, term, entry, len) Write/overwrite node.log[index-1] = {term, value}; grow log_len. Persist-before-act preserved (called before the library reports success).
on_get_entry_term(ctx, index) Return node.log[index-1].term, or 0 if index==0 or index > log_len (the term 0 = absent convention).
on_send_append_entries(ctx, peer, prev_log_index, prev_log_term, leader_commit, ...) Push an AE-request raft_sim_msg_t onto cluster.bag[] honoring partitions.
on_truncate_from(ctx, index) Set node.log_len = index - 1 (delete index..end).
on_commit_advanced(ctx, commit_index) Set node.commit_index = commit_index; apply node.log[k].value into node.applied[k] for each newly committed k.
on_send_vote_request(ctx, peer, term) (existing) Push a vote-request message onto the bag.

Message bag (mirrors raft.tla messages)

typedef enum {
    RAFT_SIM_MSG_VOTE_REQ, RAFT_SIM_MSG_VOTE_RSP,
    RAFT_SIM_MSG_AE_REQ,   RAFT_SIM_MSG_AE_RSP,
} raft_sim_msg_kind_t;

typedef struct {
    raft_sim_msg_kind_t kind;
    int      src, dst;
    uint64_t term;            /* RPC term (all kinds) */
    /* AE request */
    uint64_t prev_log_index, prev_log_term, leader_commit;
    uint64_t entry_term, entry_value; int entries_len; /* 0=heartbeat, 1=one entry */
    /* responses */
    int      granted;         /* vote rsp */
    int      success;         /* AE rsp */
    uint64_t match_index;     /* AE rsp */
} raft_sim_msg_t;
  • raft_sim_bag_push / raft_sim_bag_deliver(i) (route message i to the matching handler and push any reply) / raft_sim_bag_drop(i) / raft_sim_bag_duplicate(i) / reorder (deliver in PRNG-chosen order). Delivery honors node.partition (a partitioned endpoint's messages are not delivered, mirroring a dropped network edge).
  • A handler reply is itself pushed onto the bag as a *_RSP message, so responses are first-class bag members (drop/dup/reorder apply to them too).

Action scheduler

/* One step of the Next interleaving. Picks an enabled action from the PRNG,
 * records it, applies it through the library entry points / bag, then runs
 * raft_sim_check_all. Returns 0 on success, <0 (and dumps the trace) on the
 * first invariant violation. */
int raft_sim_step(raft_sim_cluster_t *c);

/* Run up to max_steps (or until quiescent). Returns 0 if no invariant was
 * violated through the whole run; <0 on the first violation. */
int raft_sim_run(raft_sim_cluster_t *c, int max_steps);

/* Seeded init: builds N nodes wired to the in-memory adapter + bag. */
int raft_sim_conformance_init(raft_sim_cluster_t *c, int n_nodes,
                              uint32_t election_timeout_ms, uint64_t seed);

The action set the scheduler chooses from (each maps to a raft.tla Next disjunct): Restart, Timeout, RequestVote(deliver vote-req), BecomeLeader(deliver enough vote-rsp), ClientRequest, AppendEntries, AdvanceCommitIndex, Receive(deliver an AE req/rsp incl. UpdateTerm/DropStaleResponse), DuplicateMessage, DropMessage. Only enabled actions are eligible (e.g. ClientRequest/AppendEntries require a leader; Receive requires a non-empty bag). Note that BecomeLeader is not a standalone library entry point: it is realized by delivering the quorum-completing vote-response to raft_on_vote_reply, which returns RAFT_BECAME_LEADER when that response carries the candidate over quorum.

Invariant checkers

int raft_sim_check_election_safety(const raft_sim_cluster_t *c);      /* R3.1 */
int raft_sim_check_log_matching(const raft_sim_cluster_t *c);         /* R3.2 */
int raft_sim_check_leader_completeness(const raft_sim_cluster_t *c);  /* R3.3 */
int raft_sim_check_state_machine_safety(const raft_sim_cluster_t *c); /* R3.4 */
int raft_sim_check_all(const raft_sim_cluster_t *c);                  /* R3.5: first failure */

Checker semantics (observable-state-only, R3.6):

  • Election Safety — for each term t, count nodes with role==LEADER && term==t; fail if any count > 1.
  • Log Matching — for every node pair (i, j) and every index k present in both: if log_i[k].term == log_j[k].term, then every entry at indices 1..k must be equal (term, value) in both logs; fail otherwise. Note: the library collapses raft.tla's truncate-only conflict step and the immediately-following no-conflict append into a single AppendEntries handler invocation (truncate then append), so the Log-Matching / divergent-suffix checker authors should expect the divergent suffix to be truncated and replaced with the leader's entry in one step rather than over two.
  • Leader Completeness — track the highest committed entry observed cluster-wide; for every node currently LEADER (and across forced leader changes, the highest-term leader to date), every committed (index, term) must be present in its log; fail otherwise. (Committedness is taken from node.commit_index produced by the library-gated raft_advance_commit.)
  • State Machine Safety — for every index k applied by two nodes, applied_i[k] == applied_j[k]; fail otherwise.

Trace recorder

raft_sim_action_t { kind, actor, msg_index, term, index } recorded per step into cluster.trace[]; raft_sim_dump_trace(c, fp) prints seed, n, the failing invariant, and the ordered actions in a human-readable form (R5.1, R5.2). Replay = re-run raft_sim_conformance_init with the same (n, seed) and the same max_steps (R5.3); quiet on success unless RAFT_SIM_VERBOSE (R5.4).

Deliberately-broken-build fault switch (test-only)

A runtime fault-injection flag (cluster.fault_inject, set via raft_sim_set_fault_inject) gates harness-side adapter corruptions that emulate the bug-851 defects without touching raft.c. The flag is compiled only under XCE_TESTING (never in the shipped build) and defaults to OFF (never enabled in the default CI run), so it satisfies R7.3 by the same substance a compile-time macro would — but, unlike a #ifdef, a runtime flag can be toggled within a SINGLE binary, which R7.4 requires (the negative test must assert the broken-config FAILURE and the correct-config PASS in one test). The RAFT_SIM_BREAK_* names are the flag's bit values:

  • RAFT_SIM_BREAK_TERM_STAMP — on_persist_entry writes term = 0 instead of the supplied term (emulates G1: entry term always 0), so on_get_entry_term can no longer distinguish (term=A, idx=k) from (term=B, idx=k).
  • RAFT_SIM_BREAK_TRUNCATE — on_truncate_from is a no-op (emulates G3: the divergent suffix is never deleted).

With a fault bit set the run must trip Log Matching / Leader Completeness / State Machine Safety; with the flag off (the default), the same run is clean. This keeps the negative test entirely inside the harness build configuration (R7.3) — the shipped protocol and the default CI run are unaffected. (Implementation note: RAFT_SIM_BREAK_TERM_STAMP is the flag used by the task-7.2 negative test because the library collapses conflict-truncate and the immediately-following append into one AppendEntries handler invocation, so a no-op truncate alone is overwritten by the re-persist and does not diverge through normal replication — the term-stamp corruption reliably trips Log Matching instead.)

Why adapter-side and not a raft.c edit: the harness owns only raft_sim.c/tests. Emulating G1 by having the adapter drop the term reproduces the exact observable divergence (same-index/different-term entries become indistinguishable) that the real bug caused, while honoring the spec boundary (no protocol modification). It still proves the checkers have teeth: they catch the divergence regardless of where it originates.

Optional TLC-consumable trace export

raft_sim_export_trace(c, fp) (off unless RAFT_SIM_EXPORT) emits, per step, the action and the resulting tracked variables (messages summary, per-node currentTerm/state/ log/commitIndex) named per raft.tla (R8.1, R8.2), in a stable line-oriented format the maintainer can post-process for TLC cross-checking. Off by default (R8.3).

Data Models

Domain Model

  • Bag message raft_sim_msg_t — a single in-flight RPC (vote/AE, request/response), the unit Drop/Duplicate/Reorder operate on.
  • Log entry (sim) raft_sim_log_entry_t { uint64_t term; uint64_t value; } — index is the 1-based array position (= WAL LSN); value is a synthetic monotone client value so State Machine Safety divergence is observable.
  • Action record raft_sim_action_t — (kind, actor, msg_index, term, index), the replayable trace unit.

Logical Data Model

  • raft_sim_node_t gains log[RAFT_SIM_MAX_LOG], log_len, commit_index, applied[RAFT_SIM_MAX_LOG], and a persisted-(term, votedFor) shadow for Restart.
  • raft_sim_cluster_t gains bag[RAFT_SIM_MAX_MSGS] + bag_count, the PRNG state, the seed, and trace[RAFT_SIM_MAX_STEPS] + trace_len.
  • Fixed-size arrays only (no allocation), bounded by RAFT_SIM_MAX_LOG/MSGS/STEPS, keeping the harness allocation-free and ASAN-clean.

Data Contracts & Integration

  • Entries handle: one entry per AE (entries_len ∈ {0,1}), matching the upstream raft.tla "≤1 entry" simplification and the log-replication wire shape — the harness reuses that shape exactly.
  • term 0 sentinel: honored by on_get_entry_term for absent indices.
  • 1-based index = LSN: node.log[index-1] is the canonical mapping.

Error Handling

Error Strategy

The harness is test code: on an invariant violation it dumps the seed + trace and fails the Unity assertion (the test aborts), never the library (raft.c returns status codes only — "controller never self-terminates" is preserved; the harness's halt is a test failure, not a library abort).

Error Categories and Responses

  • Invariant violation → raft_sim_check_all returns the failing invariant; the scheduler dumps (seed, n, invariant, trace) and returns <0; the test fails (R3.5, R5.1).
  • Bag overflow / log overflow (a scenario exceeded a fixed bound) → the harness fails loud (a distinct, non-invariant test error) rather than silently truncating, so bounds bugs are visible.
  • Misuse (e.g. ClientRequest driven on a non-leader) → the scheduler only selects enabled actions, so the library's -EPERM path is exercised intentionally (a targeted unit test), never as an accidental scheduler state.

Monitoring

Reuse the existing per-node trace_buf and the library on_trace events ("ae_recv", "ae_conflict_truncate", "term_adopt_ae", "ae_reply_advance", etc.) plus the new harness-level action trace, so a failing run shows both the library's view and the scheduler's interleaving.

Testing Strategy

TDD-mandatory (testing.md): every checker and scenario is written as a RED test in test_raft.c (with the raft_sim.c backing) that fails before the harness logic exists and passes after. All tests are XCE_TESTING-gated and run via /xce-build lib.

Unit tests (checkers in isolation)

  1. Each checker flags a hand-constructed violating cluster and passes a valid one: two leaders same term (Election Safety); same (idx, term) with different prefix (Log Matching); a committed entry missing from a higher-term leader (Leader Completeness); divergent applied[k] (State Machine Safety). (R3.1–3.4)
  2. raft_sim_check_all returns the first failing invariant and halts (R3.5).

Scenario tests (targeted, R4)

  1. Partition/heal: isolate a minority during appends, heal, drain; assert all four invariants hold throughout and after convergence (R4.1).
  2. Restart churn: restart nodes mid-replication preserving persisted state; assert re-convergence with no violation (R4.2).
  3. Drop/dup/reorder: perturb bag delivery; assert idempotent convergence + invariants (R4.3).
  4. Figure-8: a previous-term entry on a quorum, leader change; assert it is not reported committed until a current-term entry commits (R4.4).
  5. Stale-rejoin (bug-851 G5): a term-lagging node rejoins under a higher-term leader; assert it adopts the higher term from the AE/heartbeat path and does not re-elect at a reused term (R4.5).

Randomized + CI (R6)

  1. M-seed sweep: run raft_sim_run for a fixed max_steps across M seeds; assert zero violations. Bounded so the CI target fits the library test-suite budget (R6.4).
  2. Runs clean under ASAN/UBSAN (R6.3).

Negative test (R7)

  1. With RAFT_SIM_BREAK_TERM_STAMP (or RAFT_SIM_BREAK_TRUNCATE) set, the Figure-8 / divergent-suffix scenario fails an invariant and the trace is dumped; with the macro off, the same scenario passes — both directions asserted in one test, proving the oracle's sensitivity (R7.1, R7.2, R7.4). The macro is confined to the test build (R7.3).

Replay test (R5)

  1. A run that fails for seed S reproduces the identical failing action and invariant when re-run with seed S and the same max_steps (R5.3).