eta_run (eta v0.1.0)
Copy MarkdownThe run driver — Phase 3 of the DST framework
(design: docs/design.md).
Turns a seed into a run: start the clock, start the system, then alternate between injecting client operations, stepping one process at a time, and letting virtual time pass — checking the invariants throughout, and recording enough to replay the whole thing exactly.
The system under test supplies six callbacks; see eta_harness.
#{outcome := ok} = eta_run:run(my_sut, #{seed => 7, max_ops => 40}).The three things a run can do, and why the choice matters
At every iteration the driver picks one of:
- step a runnable process, chosen from the seeded RNG;
- inject the next generated operation;
- advance the clock to the next timer deadline.
The interesting knob is what to do when nothing is runnable. Always injecting
there is the obvious choice and it is wrong: it means the system is never left
alone with only its own timers for company, and a whole class of defect lives
exactly there. A replicated registry's traffic-triggered resync gap only shows when
nothing else is happening — a follower that lost the tail of the replication
stream detects it on the next batch, so with a client always poking the system the
gap is papered over before it can be observed. quiet_p is the probability of
letting time pass instead, and it is the reason that class of bug is reachable.
Determinism
Everything that varies is drawn from one seeded rand state: the scheduling
choices, the decision between stepping and injecting, and whatever generate/2
draws. Given the same seed and the same system, a run is reproducible.
Replay does not depend on that reproducibility. replay/3 follows a recorded
trace — {step, Id}, {op, Op} and {clock, Ms} entries, in order — so a trace
that has been edited or shrunk replays as faithfully as one straight from a seed,
which is what Phase 4 needs. A recorded step naming a process that is not runnable
is reported as a divergence rather than skipped, because a "replay" that quietly
does something else is worse than no replay.
An entry that created processes also records their ids, as a third element:
{op, Op, [3, 4]}. A replay hands those back to the scheduler rather than
recounting, so deleting one entry cannot rename the processes another entry names
— which is what lets eta_shrink delete an operation and have the rest of the
trace still mean what it meant. Entries that created nobody keep the plain two
element shape, so match with action/1 rather than on the tuple. See
eta_sched:pin/2.
All three of the driver's actions are entries, letting time pass included. A
trace missing the clock advances is not a trace of a system that has timers: replay
walks only what it is given, so the clock never moves, nothing ever becomes
runnable, and every recorded step is refused. See idle/1.
Ordering at startup
The clock starts before the system, always. A timer armed while eta_time is
inert goes to the real clock and stays there until it fires and re-arms, so
long-period timers — the interesting ones — would silently never be virtual. This
is why init/2 is called by the driver rather than by the caller beforehand.
This documentation is LLM-generated. See the AI disclosure in README.md.
Summary
Functions
What an entry did, without who it created: {op, Op}, {step, Id},
{clock, Ms} or {final, Settled}.
Whether this run's seed means anything.
Replays a fixture and compares the outcome with the one recorded when it was saved.
The processes an entry created, oldest first, and [] for the entries that
created none.
Reads a fixture without running it. Raises on an unreadable or stale file.
Load every module of the named applications, plus kernel, stdlib and eta.
Replays a recorded trace instead of generating one.
Replays a fixture and returns the full result, using the harness and options it was saved with.
Runs Mod under a seed and returns what happened.
Writes a trace to disk as a self-contained reproduction, after checking that it still reproduces.
Spawns a process to carry out an operation. Call this from execute/2 rather than
spawn/1.
Any trace-carrying result, with the trace replaced by its length. What you want when printing.
Types
-type created() :: [eta_sched:id()].
-type entry() :: {op, eta_harness:op()} | {op, eta_harness:op(), created()} | {step, eta_sched:id()} | {step, eta_sched:id(), created()} | {clock, integer()} | {clock, integer(), created()} | {final, eta_harness:settled()}.
-type fixture() :: #{version := pos_integer(), harness := module(), trace := [entry()], opts := map(), outcome := outcome(), saved := calendar:datetime()}.
-type outcome() :: ok | {violation, eta_harness:violation()} | {error, term()}.
-type result() :: #{outcome := outcome(), seed := integer(), trace := [entry()], steps := non_neg_integer(), ops := non_neg_integer(), clock_ms := integer(), skipped := non_neg_integer(), modules_loaded := [module()], stray_timers := non_neg_integer(), net := #{atom() => non_neg_integer()}, sched := #{atom() => term()}}.
Functions
What an entry did, without who it created: {op, Op}, {step, Id},
{clock, Ms} or {final, Settled}.
Match on this rather than on the entry, because an entry that created processes carries a third element and one that did not does not:
Ops = [Op || E <- Trace, {op, Op} <- [eta_run:action(E)]].
Whether this run's seed means anything.
ok = eta_run:audit(eta_run:run(my_harness, Opts)).Several fields in a result say "part of this interleaving was decided by wall clock rather than by the schedule", and a run with any of them set is one whose seed will not reproduce. They are all silent — nothing fails, nothing is logged except the scheduler's own timeout warning, and the invariants stay green.
Rather than asking every caller to know which fields those are, and to keep knowing as more are added, this checks them:
modules_loaded— code loaded mid-run, so a scheduled process made a synchronous call intocode_server. Fix withpreload.sched.cold_code— the other half of that: a process still waiting on the code server when the run ended, so the run's quiescence was a lie and the load finished too late to be inmodules_loadedat all. Same fix, and each entry names the line that reached the cold module.sched.adopted_late— processes that ran before the scheduler owned them. Fix by spawning througheta_run:spawn_op/1andeta_sched:spawn/1.sched.timeouts— steps that ended without the process reaching a receive, so it was suspended wherever it happened to be.
{suspect, Reasons} rather than {error, _} deliberately: the run happened and
its violation, if any, is real. What you cannot do is trust the seed to give it
back.
Assert on this next to your invariants. It is the single most valuable line in a simulation suite after the determinism gate itself.
-spec check_fixture(file:name_all()) -> ok | {changed, #{expected := outcome(), actual := outcome()}}.
Replays a fixture and compares the outcome with the one recorded when it was saved.
ok means the reproduction still holds. {changed, _} means the system no
longer does what it did, which is what you want to see when a fix lands — though
note that a genuine fix usually shows up as a divergence rather than a clean
run, for the reason given in save_fixture/4.
The processes an entry created, oldest first, and [] for the entries that
created none.
This is what makes a shrunk trace mean the same thing as the trace it came from —
see eta_sched:pin/2. Reading it is for diagnosis; nothing needs to write it.
-spec load_fixture(file:name_all()) -> fixture().
Reads a fixture without running it. Raises on an unreadable or stale file.
-spec preload([atom()] | false) -> ok.
Load every module of the named applications, plus kernel, stdlib and eta.
run/2 does this for you from its preload option; it is exported for code that
drives eta_sched directly, which is otherwise in exactly the position a run with
preload => false is in — and which has no modules_loaded to report the damage
afterwards.
Call it once, before there is a scheduler to be outside of. false is accepted
and does nothing, so the option value can be passed straight through.
setup_all do
:ok = :eta_run.preload([:my_app])
end
Replays a recorded trace instead of generating one.
The seed still seeds the system, but no choices are drawn from it: every step and
every operation comes from Trace.
lenient => true skips a recorded step whose process is not runnable instead of
reporting a divergence, and counts them in the result's skipped. That is what
shrinking needs and what verification must not use: removing an operation strands
the steps that belonged to it, so a strict replay answers diverged for nearly
every candidate and the shrinker learns nothing. A lenient replay's own trace is
the schedule that actually ran, which is how eta_shrink recovers a trace that
replays strictly again.
-spec replay_fixture(file:name_all()) -> result().
Replays a fixture and returns the full result, using the harness and options it was saved with.
The whole point is that a test names a file and nothing else:
#{outcome := {violation, #{property := atomicity}}} =
eta_run:replay_fixture("test/fixtures/atomicity.eta").
Runs Mod under a seed and returns what happened.
Options, all with defaults:
seed(0) — fixes the whole run.config(#{}) — passed through toinit/2.max_ops(50) — how many operations to inject before letting the system settle.max_steps(10000) — the safety bound on steps and clock advances together; hitting it is reported as{error, step_budget_exhausted}.settle_steps(2000) — how much longer to run once every operation has been injected. A system whose timers never stop — anything with a heartbeat — has no natural quiescence to wait for, and without this the only way such a run can end is the safety bound. Reaching the end of the settle phase is a normalok.op_p(0.3) — chance of injecting rather than stepping when both are possible.quiet_p(0.3) — chance of letting time pass rather than injecting when nothing is runnable. See the module doc; this is not a tuning knob so much as the thing that makes quiet-period bugs reachable.check_every(1) — run the invariants every N actions.log(true) — collect aeta_logrecord of the run.falsesuppresses the events but not the sequence numberslog/1hands out, so a harness that stamps its operations from them keeps working. Seeeta_log.net(false) — install a simulated network for the run.truefor a perfect one, or#{policy => ...}to inject loss and delay; seeeta_net. It is started beforeinit/2, seeded from the run's seed, so a fault schedule is a function of that seed and nothing else. A harness whose cluster must sync before it can survive faults leaves the policy perfect here and callseta_net:set_policy/1at the end ofinit/2.preload([]) — applications whose modules to load before the run starts. Name your own application here.kernel,stdlibandetaare always included; anything you add is loaded on top.falsedisables it entirely.This is the fix for
modules_loaded, and the only reliable one, because warming is per code path rather than per VM: running one seed does not warm the branch a later seed takes, so "run it twice" fixes one seed and not the next. Loading your application up front warms all of it.
Fields that mean the run was not deterministic
stray_timers counts timers held by a process the scheduler does not own, or
that has died. A deadline like that cannot make anything runnable, so advancing
to it would move the clock on behalf of something that can never take a step. The
driver steps over them, and reports how many it found — a non-zero count means
your system holds a timer outside the schedule, usually from a process spawned in
init/2 or one killed while blocked in a receive ... after.
sched.adopted_late counts processes that ran before the scheduler owned them,
and sched.timeouts counts steps that ended without the process reaching a
receive.
modules_loaded lists modules that were loaded while the run was in
progress, and it should be empty. Loading a module on demand is a synchronous
call into code_server, which the scheduler does not own, so a scheduled
process that reaches a module it has not touched yet blocks on something
outside the schedule. The scheduler reads that as the step ending, code_server
makes the process runnable again at a moment decided by wall clock, and every
choice after that point shifts.
The symptom is that the first run in a fresh VM produces a different trace
from every later run of the same seed. Nothing is logged, no scheduler warning
fires, and adopted_late stays 0 throughout, which is why this is reported
rather than left for you to deduce.
The fix is the preload option above. The names reported here tell you which
application to name in it, and the rule that usually identifies the culprit is
that the module which bites is the one only reachable from a scheduled
process — anything init/2 itself touches has already been loaded by the time
it matters.
The worse failure, and why preload is on by default
A process waiting on code_server is, to eta_sched, a process blocked in a
receive. It is not runnable. So if enough of the system reaches for cold code at
once, nothing is runnable, no timer is pending, and the run ends at what looks
exactly like quiescence — having done almost nothing, and reporting ok.
Measured on the 2PC harness with preloading disabled and a cold module every
client touches: 5 operations, 5 steps, nothing exited, outcome => ok. A
healthy run of the same workload takes around a hundred steps.
modules_loaded does not catch that one, because the loads complete after the
run has finished — there is nothing to report by the time the run is over. It is
the reason preload defaults to loading kernel, stdlib and eta rather than
waiting to be asked, and the reason to name your own application there even when
runs look fine.
sched.cold_code does catch it, from the other side. The scheduler looks once,
at the moment a run finds nothing runnable and is about to return, for a process
parked inside the code server's own call function — which is where a process
waiting on the code server always is, since that function is a send followed by a
one-clause receive. Each entry names the process and the frame that reached the
cold module:
#{sched := #{cold_code := [#{id := 3, pid := _, at := {my_client, commit, 2}}]}}so the symptom is no longer "a run that ended far too early with ok" and a
hunch, but a name and a line. A warning is logged too, because a run this
damaged is worth noticing without being asked.
This does not make preload optional. Detection is after the fact: the run is
already spoiled, and all cold_code buys you is knowing rather than guessing.
audit/1 checks these for you, and keeps checking them as more are added:
ok = eta_run:audit(eta_run:run(Mod, Opts)).
-spec save_fixture(file:name_all(), module(), [entry()], map()) -> {ok, outcome()} | {error, term()}.
Writes a trace to disk as a self-contained reproduction, after checking that it still reproduces.
Why not just pin the seed
Because a seed names a schedule only in the context of a particular
generate/2. Change the operation mix and every seed you pinned quietly
starts testing something else. If the test asserts on a violation it fails and
you find out; if it asserts ok it goes vacuous without a word, which is the
same silent failure as a quiescence-gated invariant that never evaluates.
A trace has no such coupling. replay/3 never calls generate/2 — it walks the
entries it is given — so a saved trace survives a rewritten workload entirely.
It also survives a different seed, since nothing is drawn from one.
Pin a seed to test that seeds reproduce. Pin a trace to regress a bug.
What is saved
The trace, the harness module, and the options. The options matter as much as
the trace: a reproduction that needs config => #{mode => broken} and is
replayed without it does not reproduce, and eta_shrink reports "nothing to
shrink" for a failure that just happened. Carrying them means a test cannot get
that wrong.
What is checked
The trace is replayed strictly before anything is written, and the outcome it produced is stored with it. So a fixture on disk is one that has been demonstrated to reproduce, rather than one that was believed to.
Take the trace from a eta_shrink:shrink/3 result whose verified is true,
which is eta_shrink's own version of this check.
What you cannot do with it
Write the mirror test. Replaying a failing trace against a fixed
implementation does not report ok — the fix changes which messages exist, so
recorded step ids stop being runnable and you get {error, {diverged, _, _}}.
"The fix works" is a claim about the whole system, and a seed sweep is the right
shape for it.
Spawns a process to carry out an operation. Call this from execute/2 rather than
spawn/1.
A plain spawn is a determinism hole, and a quiet one. The driver is not
traced, so a process it creates is not adopted by eta_sched until the driver
registers it — and in that window the new process runs on the real scheduler. One
op process racing alone is usually harmless; two of them, from operations injected
close together, race each other to deliver their first message, and the order they
arrive in is real-world timing rather than anything the seed controls. It shows up
as a seed producing two different traces, which is the framework failing at the one
thing it exists to do.
The process spawned here blocks before running Fun, so it cannot act before it is
owned. eta_run releases it once registration is done, and from that point the
scheduler decides when it runs, like every other process.
Any trace-carrying result, with the trace replaced by its length. What you want when printing.
Inspecting one whole is the first thing anybody does after a first successful run, and it is useless: a 20-operation run produces a few hundred trace entries, so a shell renders the schedule and elides the fields you were looking for underneath it.
#{outcome := ok, steps := 97, trace_length := 213, modules_loaded := []} =
eta_run:summary(eta_run:run(my_harness, #{seed => 1})).Takes a eta_shrink:result/0 too, and there trace_length says something the
other fields do not: which trace you were handed. It matches shrunk when
verified is true and original when it is false, because an unverified shrink
gives the original back.
The trace itself is for later, and even then it is not what you read. eta_log
is.