A deterministic simulation tester (DST) for the Raft consensus protocol,
written in EigenScript and
ported from the Go project codekitchen/liferaft.
This is not a polished Raft library. It is a workload that stresses the
EigenScript runtime along axes the rest of the ecosystem doesn't touch: a
long-lived, fragmenting object graph (a whole simulated cluster), a churning
event-queue heap under irregular insert/extract-min pressure, and a hard
byte-for-byte replay requirement across the entire cluster from a single
integer seed. Every divergence from the Go reference, and every leak of
nondeterminism, is a candidate EigenScript bug — logged in
FINDINGS.md, which is a primary deliverable.
- The whole simulation is reproducible from one integer seed.
- All randomness flows through one seeded PRNG (
src/prng.eigs), implemented in pure double arithmetic — norandom, no clock, no nondet builtin, no bitwise ops. Same seed ⇒ byte-identical run on any platform. - Dict iteration order is deterministic in EigenScript (
keys ofis insertion-ordered), but anything order-sensitive iterates an explicit ordered list; each such site is commented. - Two determinism checks: (a) the strong oracle — run a seed in two fresh
processes and
diffstdout; (b) the trace oracle —EIGS_TRACEthenEIGS_REPLAYmust replay byte-for-byte (and, since the sim uses no nondet builtin, the tape must contain zeroNrecords — itself an assertion that nothing nondeterministic crept in).
| Path | What |
|---|---|
src/prng.eigs |
seeded PRNG (the one source of randomness) |
src/raft.eigs |
the pure Raft state machine — handle_event(raft, event) → updates |
src/invariants.eigs |
the seven TLA+-derived invariants |
src/adversary.eigs |
seeded network adversary (latency/drop/dup/crash/reorder) |
src/cluster.eigs |
in-memory cluster harness on the runtime's cooperative task layer (a task per node, a detached deliverer task per in-flight message, virtual-clock latency, seeded-scheduler reorder) |
liferaft.eigs |
CLI runner |
test/ |
unit + determinism + replay tests |
FINDINGS.md |
every runtime bug / nondeterminism / perf cliff this port exposed |
Build EigenScript and point eigs at the binary (the repo ships a dev symlink,
gitignored):
ln -sf /path/to/EigenScript/src/eigenscript ./eigs
./eigs test/test_prng.eigs # PRNG determinism self-test
./eigs test/test_raft_unit.eigs # state-machine election unit tests
The CLI: eigenscript liferaft.eigs --seed N --steps M [--replay tape].
Milestones 1–4 complete — the full DST. Verified by test/run.sh:
-
M1 leader election — PRNG determinism, the task-based delivery layer, state-machine election unit tests, 3-node integration, same-seed two-process determinism,
EIGS_TRACE/EIGS_REPLAYbyte-for-byte (the only tape record isargs' argv, by upstream contract). -
M2 log replication — client applies, commit propagation, applied-stream safety; commands replicate to every node; 50-seed × 200-step invariant sweep.
-
M3 network adversary — latency, reordering, duplication, drops, and crash/restart, all from the one seed. Under full chaos the cluster still elects leaders (repeatedly), replicates, and commits hundreds of commands with all seven invariants + applied-stream safety holding every step. Determinism holds under chaos: same seed in two processes is byte-identical (5 seeds × 400 steps), and a 40-seed × 600-step × 5-node adversary sweep is clean. ASan-clean throughout (incl. crash/restart churn).
-
M4 chaos sweep + minimal-reproducing-seed reporting (
liferaft_sweep.eigs): sweeps seeds 1..N under the adversary, checking all invariants every step; on the first failure it reports the smallest failing seed and the first (minimal) violating step, then re-runs that exact(seed, steps)to verify the minimal repro and prints the runnable command. Validated both ways: the correct port sweeps clean (40 seeds × 600 steps), and an injected fault (--fault uptodate, a stale candidate winning — a real Raft safety bug) is caught and shrunk to a verified--seed 1 --steps 75repro.
The DST is complete. Possible extensions: snapshotting, membership changes, larger automated sweeps in CI.
In: pure in-process deterministic simulation. Out: real networking, disk persistence, the KV-store CLI, and Maelstrom/Jepsen integration.