Part of the V&V coverage initiative.
Problem
relay is stream-native: components are wired as stream<T> inputs/outputs with backpressure. Lean proves output_count ≤ n·K per engine (proofs/lean/BackpressureSafety.lean). Kani (separate issue) will verify per-engine state machines. What neither covers: concurrent producer/consumer interleavings on the stream channels themselves.
tokio-rs/loom is the right tool — it enumerates every thread interleaving for a bounded concurrent program. Note: this is the tokio-rs crate loom, NOT this org's pulseengine/loom (WASM optimizer).
Acceptance
Notes
- Keep harnesses bounded (2–3 producers, 1 consumer, ≤4 messages per producer is typically enough)
- Reference:
thrum/crates/thrum-db/tests/loom_claims.rs
- Pair with the Kani state-machine issue for complete engine coverage
Part of the V&V coverage initiative.
Problem
relay is stream-native: components are wired as
stream<T>inputs/outputs with backpressure. Lean provesoutput_count ≤ n·Kper engine (proofs/lean/BackpressureSafety.lean). Kani (separate issue) will verify per-engine state machines. What neither covers: concurrent producer/consumer interleavings on the stream channels themselves.tokio-rs/loom is the right tool — it enumerates every thread interleaving for a bounded concurrent program. Note: this is the tokio-rs crate
loom, NOT this org's pulseengine/loom (WASM optimizer).Acceptance
loomas dev-dep with#[cfg(loom)]import patterntests/loom_<channel>.rsRUSTFLAGS="--cfg loom"rivet.yaml: loom harness → Lean backpressure theoremNotes
thrum/crates/thrum-db/tests/loom_claims.rs