feat(raft-sim-conformance): bag-only Drop/Duplicate/Reorder ops (task 2.2)
This commit is contained in:
parent
ae4495104a
commit
b450e60d13
4 changed files with 238 additions and 1 deletions
|
|
@ -695,6 +695,30 @@ int raft_sim_bag_push(raft_sim_cluster_t *c, const raft_sim_msg_t *msg);
|
|||
*/
|
||||
int raft_sim_bag_deliver(raft_sim_cluster_t *c, int i);
|
||||
|
||||
/*
|
||||
* raft_sim_bag_drop: DropMessage (raft.tla:448). Discard the bag member at index
|
||||
* `i` (swap-with-last removal, bag_count -= 1) without mutating ANY node — mirrors
|
||||
* the TLA+ UNCHANGED of all non-message vars. Returns 0 on a discarded member, -1
|
||||
* (fail loud, bag untouched) on an out-of-range index.
|
||||
*/
|
||||
int raft_sim_bag_drop(raft_sim_cluster_t *c, int i);
|
||||
|
||||
/*
|
||||
* raft_sim_bag_duplicate: DuplicateMessage (raft.tla:443). Re-enqueue a copy of the
|
||||
* bag member at index `i` onto the tail (multiplicity += 1) without mutating ANY
|
||||
* node. Honors RAFT_SIM_MAX_MSGS (fail loud on overflow). Returns -1 on an
|
||||
* out-of-range index, otherwise the push status (0 on success, -1 on bag overflow).
|
||||
*/
|
||||
int raft_sim_bag_duplicate(raft_sim_cluster_t *c, int i);
|
||||
|
||||
/*
|
||||
* raft_sim_bag_pick: Reorder source. Return a PRNG-chosen in-flight bag index in
|
||||
* [0, bag_count) so delivery order is seed-deterministic (replayable) rather than
|
||||
* FIFO. Pure read: advances only c->prng, never any node state. Returns -1 when the
|
||||
* bag is empty. The caller delivers the chosen index via raft_sim_bag_deliver.
|
||||
*/
|
||||
int raft_sim_bag_pick(raft_sim_cluster_t *c);
|
||||
|
||||
/*
|
||||
* raft_sim_dump_log: print trace logs for all nodes to fp.
|
||||
* If RAFT_SIM_VERBOSE env var is set, always prints.
|
||||
|
|
|
|||
|
|
@ -698,6 +698,56 @@ int raft_sim_bag_deliver(raft_sim_cluster_t *c, int i)
|
|||
return 0; /* unreachable — enum is exhaustive */
|
||||
}
|
||||
|
||||
/*
|
||||
* raft_sim_bag_drop: DropMessage (raft.tla:448). Discard the bag member at `i`
|
||||
* (swap-with-last removal, bag_count -= 1) without touching ANY node. Mirrors the
|
||||
* TLA+ UNCHANGED <<serverVars, candidateVars, leaderVars, logVars>>: this is a
|
||||
* pure bag mutation. Bounds-checked; returns -1 (fail loud, bag untouched) on an
|
||||
* out-of-range index, 0 on a discarded member.
|
||||
*/
|
||||
int raft_sim_bag_drop(raft_sim_cluster_t *c, int i)
|
||||
{
|
||||
if (i < 0 || i >= c->bag_count)
|
||||
return -1; /* fail loud — no silent no-op */
|
||||
|
||||
raft_sim_bag_remove_at(c, i); /* swap-with-last; decrements bag_count */
|
||||
return 0;
|
||||
}
|
||||
|
||||
/*
|
||||
* raft_sim_bag_duplicate: DuplicateMessage (raft.tla:443). Re-enqueue a COPY of the
|
||||
* bag member at `i` onto the tail (multiplicity += 1) without touching ANY node —
|
||||
* mirrors the TLA+ UNCHANGED of all non-message vars. Honors RAFT_SIM_MAX_MSGS via
|
||||
* raft_sim_bag_push (fail loud on overflow). The original at `i` is left intact.
|
||||
* Returns -1 on an out-of-range index, the push status otherwise (0 on success,
|
||||
* -1 on bag overflow).
|
||||
*/
|
||||
int raft_sim_bag_duplicate(raft_sim_cluster_t *c, int i)
|
||||
{
|
||||
if (i < 0 || i >= c->bag_count)
|
||||
return -1; /* fail loud — no silent no-op */
|
||||
|
||||
/* Copy by value FIRST: raft_sim_bag_push may grow the array, but the source is
|
||||
* already an independent local, so a tail push can never alias the source. */
|
||||
raft_sim_msg_t copy = c->bag[i];
|
||||
return raft_sim_bag_push(c, ©);
|
||||
}
|
||||
|
||||
/*
|
||||
* raft_sim_bag_pick: Reorder source. Return a PRNG-chosen in-flight bag index in
|
||||
* [0, bag_count) so the scheduler delivers in a deterministic, seed-replayable
|
||||
* order rather than FIFO. Pure read of the bag: advances only the cluster PRNG, never
|
||||
* any node's (term, role, votedFor, log). Returns -1 when the bag is empty (nothing
|
||||
* to deliver). The subsequent raft_sim_bag_deliver does the node-side work.
|
||||
*/
|
||||
int raft_sim_bag_pick(raft_sim_cluster_t *c)
|
||||
{
|
||||
if (c->bag_count <= 0)
|
||||
return -1; /* empty bag — nothing to pick */
|
||||
|
||||
return (int)(raft_sim_prng_next(c) % (uint64_t)c->bag_count);
|
||||
}
|
||||
|
||||
void raft_sim_start_all_elections(raft_sim_cluster_t *c)
|
||||
{
|
||||
for (int i = 0; i < c->n; i++)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue