Skip to main content

Module compiled

Module compiled 

Source
Available on 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:

  1. 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.
  2. 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) under CompiledSim::exhaustive fork the search on a bolero decision: one instance performs the check and then ends (via a discard panic, like sim::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, and collect_sorted in 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 (see guard_not_poisoned), because a failure observed after the forced overrun could have been caused by it and attributed to the wrong assertion.

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§

CompiledSim
A handle to a compiled Hydro simulation, which can be instantiated and run.
CompiledSimInstance
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.