shadaj · GitHub

@shadaj

This introduces a deterministic simulator for Hydro that can simulate various asynchronous scenarios to identify bugs in code that use non-deterministic operators, such as `batch`. This PR focuses on just the infrastructure and support for simulating `batch` on a totally-ordered, exactly-once stream. Support for additional non-deterministic operators will follow in separate PRs (currently, an exception is thrown to prevent use of the simulator on programs that use such operators).
The simulator's job is to explore the space of potential asynchronous executions. Because "top-level" operators guarantee "eventual determinism" (per Flo), we do not need to simulate every possible interleaving of message arrivals and processing. Instead, we only need to simulate sources of non-determinism at the points in the program where a user intentionally observes them (such as `batch` or `assume_ordering`).
When compiling a Hydro program for the simulator, we emit several DFIR programs. One of these is the `async_dfir`, which contains all asynchronously executed top-level operators in the Hydro program. Again, thanks to Flo semantics, we do not need to simulate the behavior of executing these operators on different prefixes of the input, since we know that none of the downstream operators change their behavior based on the provided prefix (this is somewhat more complicated for unbounded singletons, whose intermediate states are affected by the set of elements processed in each batch, but we will address this separately).
Because each tick relies on a set of decisions being made to select their inputs (`batch`, `snapshot`), we emit each tick's code into a separate DFIR graph. The top-level simulator then schedules (`LaunchedSim::scheduler`) the async graph and tick graphs by always trying to make progress with the async graph first (so that we have the full set of possible inputs at each batch boundary), and when the async graph cannot make any further progress it selects one of the ticks, makes a batching decision for each of its inputs (`autonomous_decision`), and then executes the tick.
The selection of which tick to run and which elements to release in each batch are driven by a source of non-determinism, which is either:
a) libfuzzer (if using `.sim().fuzz` and running with `cargo sim`)
b) a RNG with 8192 iterations (if using `.sim().fuzz` and running with `cargo test` and no reproducer is available)
c) a static input of decisions (if using `.sim().fuzz` and running with `cargo test` and a reproducer is available)
d) an exhaustive, depth-first search algorithm (if using `.sim().exhaustive` and running with `cargo test`)
Whenever a fuzzer finds a failure, it stores the sequence of decisions that leads to the crash in a `.bin` file as a reproducer, so that we can re-execute quickly in testing environments.
Because Hydro uses a staged compilation model, our approach to compiling and executing the Hydro program is also a bit unique. Because the fuzzer needs to track branch coverage inside the Hydro program to be effective, and because we need low-latency interactions between the user assertions and the Hydro code, we cannot run the compiled program in a separate process. Instead, we compile the Hydro code into a _shared library_ and dynamically load it into the host process (which has the testing code). The shared library only provides the compiled DFIR graphs, so the simulator scheduler runs in the host process to enable low-latency switching between the DFIR and testing code.
This PR includes a couple of toy examples testing the simulator's functionality. Of particular interest is `sim_crash_with_fuzzed_batching`, which takes forever with an exhaustive search but quickly finds a failure case with a fuzzer.

Read the original on github.com ↗