feat(raft-sim-conformance): add conformance-harness data types to raft.h (task 1.1)
This commit is contained in:
parent
2b15dfb67a
commit
35c012ddc2
3 changed files with 179 additions and 1 deletions
|
|
@ -444,6 +444,16 @@ void raft_snapshot(const raft_state_t *s, raft_snapshot_t *snap);
|
|||
/* Upper bound on buffered AppendEntries awaiting delivery (mirrors pending[]). */
|
||||
#define RAFT_SIM_MAX_AE 64
|
||||
|
||||
/* ---- conformance harness bounds (raft-sim-conformance) ----
|
||||
* Capacity of the unified message bag (cluster.bag[], mirrors raft.tla's
|
||||
* `messages`): in-flight vote/AE requests and responses, the unit on which
|
||||
* Drop/Duplicate/Reorder operate. Sized generously above RAFT_SIM_MAX_AE so a
|
||||
* bounded run never overflows the bag (duplicates add members). */
|
||||
#define RAFT_SIM_MAX_MSGS 256
|
||||
/* Upper bound on recorded scheduler steps (cluster.trace[]) for replayable
|
||||
* failure traces. One raft_sim_action_t is recorded per step. */
|
||||
#define RAFT_SIM_MAX_STEPS 1024
|
||||
|
||||
/* Buffered RPC entry: one pending vote-request to route.
|
||||
* last_log_term/last_log_index capture the CANDIDATE's advertised last-log tuple
|
||||
* at SEND time (mirroring raft_sim_ae_t.leader_term) so the (lastLogTerm,
|
||||
|
|
@ -487,6 +497,76 @@ typedef struct {
|
|||
size_t entry_len; /* valid when n_entries == 1 */
|
||||
} raft_sim_ae_t;
|
||||
|
||||
/* ---- conformance harness data types (raft-sim-conformance) ----
|
||||
*
|
||||
* These mirror raft.tla's `messages` bag and per-node variables for the
|
||||
* deterministic conformance/verification harness. They are SEPARATE from the
|
||||
* byte-payload WAL model above (raft_sim_entry_t / raft_sim_ae_t / raft_sim_rpc_t):
|
||||
* the conformance harness uses a lightweight (term, value) log entry and a single
|
||||
* unified message type so a randomized, seeded action scheduler can drive N library
|
||||
* instances purely synchronously and assert the four Raft safety invariants. */
|
||||
|
||||
/* Unified bag-message kind: a vote/AE request or its matching response. */
|
||||
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;
|
||||
|
||||
/* One in-flight RPC in the message bag (mirrors raft.tla `messages`). Carries the
|
||||
* union of vote/AE request and response fields; only the fields relevant to `kind`
|
||||
* are meaningful. This is the unit Drop/Duplicate/Reorder operate on; a handler
|
||||
* reply is pushed back as a *_RSP member so responses are first-class. */
|
||||
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; /* one entry per AE (raft.tla "<=1 entry") */
|
||||
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;
|
||||
|
||||
/* One conformance-harness log entry: term stamp + synthetic monotone client value.
|
||||
* The 1-based array position is the log index (= WAL LSN); `value` makes State
|
||||
* Machine Safety divergence observable. Distinct from raft_sim_entry_t (which models
|
||||
* the byte-payload WAL): this is the (term, value) bag/applied model. */
|
||||
typedef struct {
|
||||
uint64_t term;
|
||||
uint64_t value;
|
||||
} raft_sim_log_entry_t;
|
||||
|
||||
/* The Next-action set the scheduler chooses from; each maps to a raft.tla `Next`
|
||||
* disjunct. Only *enabled* actions are eligible at a given step. */
|
||||
typedef enum {
|
||||
RAFT_SIM_ACT_RESTART, /* Restart: re-init preserving persisted state */
|
||||
RAFT_SIM_ACT_TIMEOUT, /* Timeout: become candidate, bump term */
|
||||
RAFT_SIM_ACT_REQUEST_VOTE, /* RequestVote: deliver a vote-request */
|
||||
RAFT_SIM_ACT_BECOME_LEADER, /* BecomeLeader: deliver quorum-completing vote-rsp */
|
||||
RAFT_SIM_ACT_CLIENT_REQUEST, /* ClientRequest: leader appends a client value */
|
||||
RAFT_SIM_ACT_APPEND_ENTRIES, /* AppendEntries: leader pushes an AE-request */
|
||||
RAFT_SIM_ACT_ADVANCE_COMMIT, /* AdvanceCommitIndex: leader advances commit */
|
||||
RAFT_SIM_ACT_RECEIVE, /* Receive: deliver a bag message to its handler */
|
||||
RAFT_SIM_ACT_DUPLICATE_MESSAGE, /* DuplicateMessage: re-push a bag member */
|
||||
RAFT_SIM_ACT_DROP_MESSAGE, /* DropMessage: discard a bag member */
|
||||
} raft_sim_action_kind_t;
|
||||
|
||||
/* One replayable trace unit: the action taken at a scheduler step plus the operands
|
||||
* needed to reproduce it (actor node, target message index in the bag, and the
|
||||
* (term, index) the action referenced). Recorded per step into cluster.trace[]. */
|
||||
typedef struct {
|
||||
raft_sim_action_kind_t kind;
|
||||
int actor; /* node that took the action (-1 if N/A) */
|
||||
int msg_index; /* bag index acted on (-1 if N/A) */
|
||||
uint64_t term; /* term referenced by the action (0 if N/A) */
|
||||
uint64_t index; /* log index referenced by the action (0 if N/A) */
|
||||
} raft_sim_action_t;
|
||||
|
||||
/* One simulated node */
|
||||
typedef struct {
|
||||
raft_state_t state;
|
||||
|
|
@ -506,6 +586,19 @@ typedef struct {
|
|||
* commit-advance DRIVER helper is a later task; this is only the callback half. */
|
||||
uint64_t commit_index;
|
||||
int commit_advanced_count;
|
||||
/* ---- conformance harness per-node state (raft-sim-conformance) ----
|
||||
* applied[k-1] holds the client value applied at committed index k (set by the
|
||||
* node's on_commit_advanced as commit_index advances). State Machine Safety
|
||||
* checks that applied[k] agrees across nodes. NOTE: log_count above already
|
||||
* 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];
|
||||
/* 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
|
||||
* live volatile state. */
|
||||
uint64_t persisted_term;
|
||||
int persisted_voted_for;
|
||||
/* per-node trace event log for test assertions */
|
||||
char trace_buf[4096];
|
||||
int trace_len;
|
||||
|
|
@ -523,6 +616,18 @@ typedef struct {
|
|||
* task 8.2); on_send_append_entries enqueues here. */
|
||||
raft_sim_ae_t ae_pending[RAFT_SIM_MAX_AE];
|
||||
int ae_pending_count;
|
||||
/* ---- conformance harness cluster state (raft-sim-conformance) ----
|
||||
* Unified message bag mirroring raft.tla `messages`: vote/AE requests and
|
||||
* responses, the unit Drop/Duplicate/Reorder operate on. */
|
||||
raft_sim_msg_t bag[RAFT_SIM_MAX_MSGS];
|
||||
int bag_count;
|
||||
/* Seeded deterministic PRNG: `seed` is the run's reproducibility key; `prng`
|
||||
* is the evolving generator state (SplitMix64/xorshift, no libc rand()). */
|
||||
uint64_t seed;
|
||||
uint64_t prng;
|
||||
/* Replayable per-step action trace for failure dumps. */
|
||||
raft_sim_action_t trace[RAFT_SIM_MAX_STEPS];
|
||||
int trace_len;
|
||||
} raft_sim_cluster_t;
|
||||
|
||||
/*
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue