stageleft_runtime and crate feature sim only.Expand description
Interfaces for compiled Hydro simulators and concrete simulation instances.
§Quiescence and observation soundness
The scheduler distinguishes two kinds of simulation work:
- Deterministic work: running the top-level async dataflows, which simply propagate
whatever data is already in flight. This makes no
nondet!decisions, so running it can never change which executions are explored. - Nondeterministic work: running ticks and observations, whose behavior depends on decisions drawn from the bolero driver (batch boundaries, snapshot versions, message orderings). Each decision forks the space of possible executions.
The simulation is quiescent when neither kind of work can make progress without new
external input. Test-side observations (the methods on SimReceiver /
SimClusterReceiver) interact with the scheduler while waiting, and the key soundness
question is: when is it okay for an observation to let nondeterministic work run?
Waiting for a message is always sound. If the message eventually arrives, the work
that ran was necessary to produce it (schedules that run extra work are also valid
executions and are explored separately). If the simulation instead quiesces without
producing the message, the assertion fails and the instance ends, so nothing can observe
the overrun. This is why SimReceiver::next, SimReceiver::collect_n, and the
assert_yields* prefix checks are safe to use in the middle of a test.
Observing the absence of a message is dangerous. Proving that “no more messages can
arrive” requires driving the simulation all the way to quiescence, running all pending
nondeterministic work. A later assertion may have needed to observe a state where that
work had not yet run — e.g., assert_yields_only([1, 2]) followed by reading a counter
must be able to see the counter before the ticks that count 1 and 2 have fired.
Forcing quiescence at the first assertion would make some executions unobservable, and
extra messages produced by the forced work could surface at a later assertion,
misattributing the failure. Absence-observing APIs therefore proceed in phases:
- Settle (see
SettlePauseGuard::poll_settle): the scheduler runs only deterministic work, pausing just before nondeterministic work. If the simulation reaches quiescence this way, the end-of-stream check is free — no decision was forced, no execution was cut off — and the test simply continues. - If nondeterministic work is pending, the check would overrun. What happens next depends
on the API and engine:
- The assertion APIs (
SimReceiver::assert_no_more,assert_yields_only*,collect_n_only) underCompiledSim::exhaustivefork the search on a bolero decision: one instance performs the check and then ends (via a discard panic, likesim::continue_if!), while sibling instances skip the check entirely and continue. The exhaustive driver enumerates the checking instance first, so a failing check is found before any instance runs past it — with a decision trace that leads exactly to the failing assertion. Since nothing after the check runs in the checking instance, the overrun it performs is unobservable, and the continuing instances never quiesce, so every downstream state remains reachable. - Otherwise (fuzz / RNG / replay engines, or the drain-everything APIs
SimReceiver::try_next,SimReceiver::collect, andcollect_sortedin every mode), the pending work runs and the instance is tainted (QuiescenceState::tainted). Reads of the now-quiescent state remain sound (they observe a fully-drained simulation that can no longer advance), so tests may drain multiple output ports at the end. But once new input is sent, the instance is poisoned (QuiescenceState::poisoned): any further receive panics (seeguard_not_poisoned), because a failure observed after the forced overrun could have been caused by it and attributed to the wrong assertion.
- The assertion APIs (
NOTE: This module runs inside bolero’s catch_unwind scope, which silently
swallows panics. Internal invariant checks should use abort_assert!
rather than panic!/assert!.
TODO(mingwei): Panics inside the tick DFIR (generated code in the dylib) are
also caught by bolero’s catch_unwind. Consider a mechanism to detect and
propagate those as well.
Structs§
- Compiled
Sim - A handle to a compiled Hydro simulation, which can be instantiated and run.
- Compiled
SimInstance - A single instance of a compiled Hydro simulation, which provides methods to interactively execute the simulation, feed inputs, and receive outputs.
Traits§
- Instantiator
- A trait implemented by closures that can instantiate a compiled simulation.
Functions§
- quiesce
- Runs the simulation to quiescence, as an explicit phase barrier between rounds of a multi-phase test.