eta_run (eta v0.1.0)

Copy Markdown

The 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

created()

-type created() :: [eta_sched:id()].

entry()

-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()}.

fixture()

-type fixture() ::
          #{version := pos_integer(),
            harness := module(),
            trace := [entry()],
            opts := map(),
            outcome := outcome(),
            saved := calendar:datetime()}.

outcome()

-type outcome() :: ok | {violation, eta_harness:violation()} | {error, term()}.

result()

-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

action/1

-spec action(entry()) -> tuple().

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)]].

audit/1

-spec audit(result()) -> ok | {suspect, [{atom(), term()}]}.

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 into code_server. Fix with preload.
  • 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 in modules_loaded at 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 through eta_run:spawn_op/1 and eta_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.

check_fixture(Path)

-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.

created/1

-spec created(entry()) -> created().

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.

load_fixture(Path)

-spec load_fixture(file:name_all()) -> fixture().

Reads a fixture without running it. Raises on an unreadable or stale file.

preload/1

-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

replay(Mod, Trace, Opts)

-spec replay(module(), [entry()], map()) -> result().

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.

replay_fixture(Path)

-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").

run(Mod, Opts)

-spec run(module(), map()) -> result().

Runs Mod under a seed and returns what happened.

Options, all with defaults:

  • seed (0) — fixes the whole run.

  • config (#{}) — passed through to init/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 normal ok.

  • 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 a eta_log record of the run. false suppresses the events but not the sequence numbers log/1 hands out, so a harness that stamps its operations from them keeps working. See eta_log.

  • net (false) — install a simulated network for the run. true for a perfect one, or #{policy => ...} to inject loss and delay; see eta_net. It is started before init/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 calls eta_net:set_policy/1 at the end of init/2.

  • preload ([]) — applications whose modules to load before the run starts. Name your own application here. kernel, stdlib and eta are always included; anything you add is loaded on top. false disables 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)).

save_fixture(Path, Mod, Trace, 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.

spawn_op(Fun)

-spec spawn_op(fun(() -> term())) -> pid().

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.

summary/1

-spec summary(map()) -> map().

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.