Skip to content

How the simulator tested the supervisor

The supervisor's safety argument is about what happens when things go wrong at the worst moment: a crash between a commit and a call, a reply lost, a call landing an hour late, two supervisors at once. Unit tests don't reach those moments, and a model check only checks a model. Model checks of the protocol did find real bugs, each now fixed. But the question that matters is whether the code does what the model does.

So the supervisor spec, 0004, stayed DRAFT until a simulator built to spec 0005 passed against the real code. It passed, and spec 0004 is APPROVED. The simulator is internal/sim, and it still runs on every merge request and every night. Run the simulator says how to use it.

What it runs

Each seed runs one job through the real Fold, Next, records, memory adapter and supervisor loop, with these simulated processes around it:

  • one to three supervisors, each calling supervise.Run on the job. A supervisor that crashes or is stopped restarts later as a new incarnation;
  • a person, issuing cancel, hold, release, requeue, resubmit and give-up through the real Operator at random moments, and answering escalations;
  • the scheduler's environment, through the memory adapter's Env: starting opened jobs, and completing, failing or preempting them, or losing a node under them;
  • trainers, publishing checkpoints for every running execution through the real checkpoint package, and for a few minutes after its object ended, as old runs do;
  • a sweeper, which, once the record has settled, stops anything of the job still alive, as a host sweeping residuals would;
  • a pruner, on seeds that run the file store, which tombstones the record a few minutes after it settles.

The job's policy is a resubmit rule for preemption and node loss, or in a quarter of seeds a hold rule for node loss. In one seed in five the job declares a shared checkpoint, so its recovery rule becomes a hold, and the memory adapter's cessation signal answers that the processes are gone.

The record store is the one a host would use in half the seeds: records/ledgerstore over go/ledger's file store, on internal/sim/crashfs and the simulated lock table (internal/sim/locktable). Each process opens the store with its own view of the disk and the locks, so a crash can land between any two filesystem calls of a commit. In a third of those seeds the lock table grants ownership to every supervisor at once, and in some the record is tampered with and must be refused. The other half use recordstest.Memory behind a fault layer.

How it stays deterministic

A failure is only useful if the seed reproduces it. The whole run is one testing/synctest bubble, so every timer and time.Now uses a fake clock that moves only when every goroutine is waiting. Each simulated process is exactly one goroutine.

Every call a process makes into a seam (the backend, the record store) parks at a yield point. The scheduler repeats one loop: wait until every goroutine is parked, choose one parked call by the seed, let it proceed. So exactly one actor moves at a time, in an order the seed decides. Between steps the scheduler may move the clock forward up to two seconds, so timers fall due.

Each process draws from its own random source, seeded from the run's seed, its process id and its incarnation, so the order of draws is the order of its own code and never Go's scheduling.

Code on the simulated path follows rules that keep this true: it starts no goroutines, ranges over maps only sorted or annotated //sim:unordered, never draws from the global random source, and decides whether a deadline has passed from the clock rather than from ctx.Err() alone. The package internal/sim/lint checks the mechanical ones over every package on the path, and the supervisor's single-select event loop is shaped by them. As a backstop each seed runs twice and the two traces' hashes must match, and a nightly shard runs under -race.

The faults

Each seed turns on a random subset of fault kinds. That finds more than turning everything on at once, which tends to drown each fault in the others.

  • Backend calls fail before taking effect, take effect and lose their reply, or land later at a moment the scheduler picks: a Start can land after a cancel or after settlement. Hold and requeue calls can start past their deadline, or land between their deadline and deadline plus CallBound.
  • Find can omit an object still being created, and its reply can arrive late.
  • Commits can take effect and lose their reply. On the file store the lost commit is retried with the same mutation id, and the machine holding the record can crash.
  • Supervisors crash (including mid-commit), stop gracefully and drain, or freeze as if SIGSTOPped while keeping their lock. Ownership can be revoked from a live supervisor.
  • The checkpoint filesystem (internal/sim/crashfs, which keeps data and directory entries durable only once synced) can lose power, keeping only what was synced.
  • Targeted faults hit a supervisor exactly where the model checks' counterexamples needed one: a freeze between its Find and its settlement commit, or a crash at a call-deadline commit.

Some classes of seed aim harder at known weak spots: frequent delayed requeues around the job's end, frequent holds with delayed placements, early cancels meeting launches in flight.

The invariants

After every step the simulator checks the record and the memory adapter's ground truth. A broken invariant ends the run with the seed and its trace. The invariants are spec 0004 D10's:

# Invariant
1 a terminal outcome never changes
2 a committed cancel blocks every later authorization
4 a lost reply never leads to an ungated launch: every opened object had an Open sent for it, or was revived by a requeue
5 nobody stops the canonical object of the running submission, except the node-loss fence
6 a retired object is never opened
7 after settlement, anything of the job alive by ground truth is gated and was never opened; under the manual policy with no Abandon, nothing is alive at all
10 the resolved checkpoint never drops below the greatest durable publication
11 at most one opened, unended object per job, by ground truth
12 a submission's canonical object never changes
13 no Open is sent from a read that saw a committed cancel
14 each attempt sends at most one Start, and no submission exceeds the retry bound
15 a hold that took effect is never undone while the record says held
16 once a cancel reports clean-up complete, nothing of the job is pending or running

Invariants 3, 8 and 9 surface as a record that can't be read or doesn't fold. One extra check holds the reconciler to its word: an object recorded as verified stopped really is stopped.

Liveness

Safety is easy if nothing happens, so every seed ends with a quiet phase. Faults stop, frozen supervisors resume, and the clock jumps half an hour so every deadline and escalation age passes at once. The simulated person answers every escalation the way a person would, and an escalation they couldn't act on, one with no cause they know, fails the run. Within the quiet bound (2,000 steps by default, four times that on the file store) the record must settle, every delayed call must have landed, and nothing of the job may be left alive.

Coverage

A clean run only means something if the faults fired. Each seed counts the events it saw. With -coverage, a batch fails if any required event never happened in a shape: a late landing, a lost reply, a crash mid-commit, a revoked owner committing, an Open landing after a cancel, a create landing after settlement, an old trainer publishing, a power cut losing unsynced data, and more; plus Slurm-only events (a requeue after the outcome, calls landing in the deadline window, a requeue bit restored, a cessation answer resuming a held job), Kubeflow-only ones (a lost node, a stop on a lost node), and file-store ones counted over the seeds that ran it (a lost commit reply retried, a machine crash, a corrupt record refused, a record tombstoned). The lists are in internal/sim/coverage.go.

The knobs

Finally, the simulator has to find the bugs already known. Each fix the model checks found has a knob in internal/mutants that reverts it: settling on a stale Find, opening N+1 while requeue calls are in flight, committing a call's deadline after sending it, retiring the canonical object, and eight more. In a normal build the knobs are constants set to false and compiled away. In a build tagged dispatch_mutants, TestKnobs turns each on in turn, and the simulator must find a violation within the seed budget. A knob it can't catch blocks approval, unless the maintainer accepts a written argument that the fix is defence in depth. Two were accepted, provisionally, on 2026-10-12: SingleCancelSweep and VerifiedStoppedAsEvidence. Their arguments are in acceptedExempt in internal/sim/knobs_test.go.

The approval bar

Spec 0005 set it: spec 0004 moves to APPROVED when a nightly-size batch (50,000 seeds) passes in both shapes, no coverage counter is zero for either shape, every knob is caught or accepted as exempt, and every seed passes the determinism check. A clean 50,000-seed batch at commit 13a9f4c cleared it, and spec 0005 D10's approval record holds the evidence. CI keeps running the per-merge-request and nightly batches, so a change that breaks the protocol fails there; the commands are in the how-to.