diff --git a/CHANGELOG.md b/CHANGELOG.md index b40287da..3ac64376 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,8 @@ ## Unreleased +- TESTING.md: how databases test (FoundationDB, TigerBeetle, SQLite, AWS, + Jepsen and others), how each technique maps to spawned, and the gaps. - Tests: planted-bug follow-ups. New scenario-fuzzer oracles for restart decisions, RestForOne cohorts, Transient restarts, required restarts versus budget exhaustion, backoff delays in virtual time, linked exit reasons, diff --git a/docs/TESTING.md b/docs/TESTING.md index 729688af..e6948eaa 100644 --- a/docs/TESTING.md +++ b/docs/TESTING.md @@ -102,6 +102,74 @@ suites cover faults, Kani and mutation testing harden functions and tests, and the clients and canaries check real use. A bug fix always comes with a test that reproduces it ([reproducing-test rule](#reproducing-test-rule)). +## How databases test, and how spawned compares + +Databases have the strongest testing culture in industry, because a bug +silently loses data. Spawned borrows their techniques deliberately; this +section maps each one to what spawned does and lists where it is still behind. + +### What the best databases do + +1. **Deterministic simulation (FoundationDB, TigerBeetle's VOPR).** The whole + system, including network, disk, clock and other machines, runs on one + seeded, single-threaded simulator that injects faults reality rarely + produces: machines dying mid-write, partitions, disk errors, clock jumps. + Every failure replays exactly from its seed, and simulation runs constantly. +2. **Fault injection at every point (SQLite, FoundationDB's `BUGGIFY`).** + SQLite fails every allocation, every I/O and every possible crash point in + turn and checks the database stays consistent. `BUGGIFY` points make code + misbehave on purpose under simulation. +3. **Formal specifications (AWS, MongoDB, CockroachDB, TiDB).** AWS specifies + systems such as DynamoDB and S3 in TLA+ before building them. Checking + traces of the real code against the spec keeps the two from drifting. +4. **Proving the tests work (SQLite).** About 600 lines of test per line of + code, 100% branch coverage at the machine-code level (MC/DC), and checks + that deliberately broken builds fail the suite. +5. **Fuzzing and differential or metamorphic testing (SQLite, CockroachDB, + DuckDB).** Generated workloads compared against a reference, or the same + workload under different configurations that must agree. +6. **Black-box consistency checking (Jepsen).** The real system on real + machines under partitions, crashes and clock skew; every operation's history + is checked for linearizability. +7. **Long soak and chaos runs (CockroachDB's roachtest, TiDB's Chaos Mesh).** + Days of load with injected failures, watching for leaks and slow decay. +8. **Production as the last test.** Canaries, staged rollouts and invariant + monitors on live systems. + +### What spawned does + +| Database practice | Spawned's equivalent | +|---|---| +| Deterministic simulation | The [simulator](#seeds-and-decision-tapes-under---cfg-spawned_sim): a seeded single thread with virtual time; decision tapes that replay exactly and shrink to a minimal schedule; PCT and bounded exploration. The simulated suites are a required CI check (`sim`) | +| Fault injection | Failpoints at named sites in the lifecycle code; suites that panic in every user callback and drop every public future at every await point | +| Formal specifications | TLA+ models of every lifecycle protocol, each invariant with a negative control that must fail; Apalache proofs of the safety invariants | +| Specs tied to the code | Trace validation of real runs against the models, trace coverage, and the required `model-sync` check: code that changes modelled behaviour without its model fails CI | +| Proving the tests work | The [planted-bug matrix](#planted-bug-sensitivity) (23 of 24 realistic bugs caught, each by two or more layers), `cargo-mutants`, and the [semantics coverage](#semantics-coverage) matrix (a check that fails for 47 of 50 guarantees) | +| Fuzzing, metamorphic testing | The coverage-guided [scenario fuzzer](#scenario-fuzzing-fuzz) with contract oracles; one workload on every backend must give the same result | +| Linearizability checking | A Porcupine-style checker over concurrent request histories | +| Memory-model checking | Loom, ThreadSanitizer, LeakSanitizer and Kani proofs | +| Soak and chaos | The [soak harness](#soak-harness) (hours of churn with leak gates, before each release); fault-injection canaries that crash supervised actors inside real clients | +| Production | Ethrex and Ethlambda canaries on testnet and mainnet, compared with the clients' main branches | + +### Where spawned is behind, and the plan + +1. **Simulating the environment.** FoundationDB simulates network and disk, + where most distributed bugs live. Spawned's simulator controls actors and + time only. The determinism backlog (ROADMAP tier 3: clock and randomness + interception, `spawn_blocking`, timers) and actor-owned I/O with a simulated + network (rank 22a) close this, so a whole client node with peers, + partitions and crashes can run from a seed. +2. **Volume.** FoundationDB and TigerBeetle simulate continuously. Spawned's + simulator and fuzzer run in CI and by hand; continuous seeds are the + cheapest way to find what is left once scheduled runs are enabled. +3. **Code coverage.** SQLite measures branch coverage; spawned measures + guarantee and model-action coverage. Adding code coverage of the simulated + suites would show untested paths directly. +4. **Production monitors (rank 5c).** The TLA+ invariants as live checks + inside canary nodes. +5. **An external audit.** A Jepsen-style review of the semantics contract and + the models by someone outside the project, a 1.0 requirement. + ## Verification layers Status of each layer. "Planned" items are tracked in the