Bounded black-box crash testing
12,600 crash points.
Zero corruptions.
Every I/O boundary becomes a crash point, and every un-fsynced reordering at each one is enumerated — all of them, not a sample. The same harness catches all four planted durability bugs.
A zero is only worth reading if the detector fires. That is what the fixtures below are for.
Method, not mine: bounded black-box crash testing — ALICE/BOB (OSDI 2014), CrashMonkey/ACE (OSDI 2018). Why exhaustive →
The detector, exercised
Five deliberately broken builds, and what the harness did to each
The tick on each bar is that fixture's pre-registered floor, committed before the run.
One run, every boundary
Walk a single workload, crash point by crash point
Every square is one place the machine can lose power. The selection lives in the URL, so a specific corruption is a link.
Expected
Recovered
Diff
What exhaustive costs
The reorder bound, and where the unknowns go
Above the bound, schedules are sampled rather than enumerated, and a crash point whose sample found nothing is reported unverifiable rather than clean. An absence under a sample is not evidence.
Off the model, onto the disk
Three real targets
The method is not mine
ALICE/BOB (Pillai et al., OSDI 2014) and CrashMonkey/ACE (Mohan et al., OSDI 2018) found 24 crash-consistency bugs in production Linux filesystems, one in a formally verified one. Their finding — that such bugs overwhelmingly reproduce in three operations or fewer — is what makes a bounded space worth enumerating instead of sampling.
What this is not
- Not a database. Single process, single writer, no concurrency model at all.
- Not a replacement for SQLite or LevelDB, and not a competitor to them: one of them is a target here.
- Not a filesystem checker. The device is modelled; its fidelity to NTFS is measured, not assumed.
- Sub-sector tearing, bit rot, and a disk that lies about
fsyncare all real and all out of scope.