Expand description
Seed, deterministic RNG, and the choice trace — the determinism contract.
Every nondeterministic scheduling decision flows through a single choke point,
Chooser::decide. In record mode it draws from a seeded RNG and logs a
ChoicePoint; in replay mode it returns the next recorded choice and
asserts the decision shape still matches (divergence detection). This is what
makes a concurrent program a deterministic function of (program, seed) and
exactly reproducible from (program, trace) — the property the interpreter,
VM, and translation validation all rely on.
Structs§
- Choice
Point - One recorded nondeterministic decision: its kind, how many options were
available, and which index was taken. This shape is intentionally
id-agnostic, so the trace format does not depend on
TaskId/ChanId/etc. - Sched
Seed - The scheduling seed. A fixed seed makes execution fully deterministic.
- Sched
Trace - A full record of the scheduling decisions a run made. Replay it for an exact re-execution, or compare two traces to detect a divergence.
- Seeded
Rng - A small, deterministic, WASM-safe PRNG (SplitMix64).
Enums§
- Choice
Kind - The class of a scheduling decision — recorded so replay can detect divergence.
- Chooser
- The decision choke point: records (seeded) or replays scheduling choices.