Skip to content

Research notes / Recovery correctness

Crash-consistency tests: the oracle is part of the result

12 October 2026 / Primary-source methods review

A successful restart is an observation, not a complete durability test. The useful question is whether the recovered state satisfies the promised contract. A test result needs its workload, fault model, explored states and correctness checker.

Start with the layer being tested

Separate three questions: can the storage structure be opened; are application relationships valid; and did a successfully acknowledged durable update survive? The first two do not answer the third. An intact older version can be the wrong result. Conversely, an update with no acknowledgement may already have persisted.

That last distinction is why the checker must describe a set of acceptable states. Demanding exactly the pre-crash bytes can reject a valid recovery; accepting anything that opens can miss data loss. Our example below makes this distinction explicit. It complements the existing guides to durable rename and failed synchronization.

Two papers, different targets

ALICE: assumptions made by an application

ALICE constructs candidate file states from an application's system-call trace and an abstract persistence model. A supplied checker tests application invariants. Its 2014 study examined 11 applications and reported 60 static vulnerabilities: these are not 60 measured failures in a production population. Multiple failing executions may map to one source-level vulnerability. The paper explicitly disclaims completeness and describes limitations for concurrent traces and file attributes.[2, sections 3-4]

CrashMonkey and ACE: bounded filesystem workloads

The 2018 study reproduced 24 of 26 collected historical bugs with workloads of at most three core operations. Setup operations are not included in that count. ACE generates bounded workloads; CrashMonkey records and replays I/O and checks persisted files after recovery. This is not a present-day filesystem ranking.[1, sections 3-6]

The B3 approach tests crashes after persistence points. It does not explore arbitrary mid-operation crashes or reorder I/O to generate additional states. Its limits include the chosen initial image and workload space. Exhaustive inside those boundaries does not mean exhaustive over all failures.[1, section 4.4]

ACE's documentation makes the counting convention operational: a sequence length counts core operations, while dependency setup and persistence calls can make the executable test longer. Report the operation alphabet, filenames, arguments and initial state, not just a sequence-length label. [6]

A process exit is not the entire fault model

SQLite's crash tests illustrate the distinction. Its documented TCL harness uses a special virtual filesystem to reorder and corrupt unsynchronized writes, then checks recovery. The TH3 harness uses an in-memory virtual filesystem and snapshots. Killing a child process without those modeled storage effects is not the same test. SQLite also describes compound tests that inject an I/O or allocation failure during recovery. [3, sections 3.3-3.4]

The rollback-journal atomic-commit description separately states storage assumptions and describes simulated partial writes and write reordering. It does not describe the WAL commit mechanism. A test result must identify both the selected mode and which lower-layer promises the simulator assumes; simulation alone cannot certify that a particular device honors them. [4, sections 2 and 8]

An executable counterexample to a weak checker

Consider an invented object with a manifest and payload. Initially both have generation 0; an update intends generation 1. Our contract requires matching generations after recovery. Before a durable acknowledgement, either complete generation is acceptable. After acknowledgement, only generation 1 is acceptable. All other application state is assumed unchanged.

The table enumerates every combination of the two generation labels and the acknowledgement flag, assuming both files can be opened. These are deliberately supplied checker inputs, not a claim that every combination is reachable on any particular filesystem. A read-only/open-only checker accepts every row.

Synthetic truth table. Generation labels are not time, and rows are not a failure-frequency sample.
Durable ack observedManifestPayloadContract result
No00Allowed
No01Reject: mixed generations
No10Reject: mixed generations
No11Allowed
Yes00Reject: acknowledged generation lost
Yes01Reject: mixed generations
Yes10Reject: mixed generations
Yes11Allowed

The old/old row changes its meaning when acknowledgement changes. The new/new row remains acceptable without an acknowledgement because completion and observation are different events. Mixed generations are rejected regardless of acknowledgement. This is a specification example, not a replacement for the application's real recovery rules.

The table is generated from the same small JavaScript oracle exercised by regression tests. Tests cover all eight readable combinations, unreadable states and malformed inputs. No disk writes, crash injection, latency measurement or paper replication occur in this example.

Check the artifact, not only the paper

One reproducibility trap is unusually concrete: the distributed ALICE documentation says its released version does not trace relevant memory-mapped writes, although the publication's implementation did. It also lists unsupported attributes and other limitations. Matching the paper title is therefore insufficient to establish matching test coverage. Pin the actual artifact and inspect its exclusions.[5, caveats and limitations]

What a useful report must preserve

For a new investigation, we propose the following acceptance record. This is a reporting protocol, not an experiment performed by Hesela:

  1. Pin the application, kernel, filesystem, mount options, device cache settings, harness revision and initial test-image hash.
  2. State the fault boundary and what is lost, preserved, reordered or torn. Keep application termination, kernel failure and modeled device power loss distinct.
  3. Record the workload bounds and excluded cases, including concurrency, allocation pressure, initial data and recovery-time failures.
  4. Preserve the acknowledgement trace independently of the storage under test. Compare recovered identities, contents and relationships against a named contract.
  5. Test the checker with known-good and deliberately bad fixtures, then retain minimized failing workloads and image hashes. Keep harness errors separate from product failures.
  6. Report the tested configurations and counterexamples. Do not turn a clean run into a universal proof or a count of failed cases into an incident rate.

These distinctions make a negative result useful: readers can see which claims were actually challenged and which remain untested. Corpus entries: bounded crash testing and crash-test oracle.

Primary sources and limits

  1. Jayashree Mohan, Ashlie Martinez, Soujanya Ponnapalli, Pandian Raju and Vijay Chidambaram. Finding Crash-Consistency Bugs with Bounded Black-Box Crash Testing. OSDI 2018, pp. 33-50; sections 3-6.
  2. Pillai et al. All File Systems Are Not Created Equal: On the Complexity of Crafting Crash-Consistent Applications. OSDI 2014; sections 3-4.
  3. SQLite project. How SQLite Is Tested, sections 3.3-3.4: crash and compound-failure tests.
  4. SQLite project. Atomic Commit In SQLite, sections 2 and 8: assumptions and simulated faults (rollback-journal mode).
  5. University of Wisconsin-Madison ADSL. ALICE user documentation: checker contract and caveats.
  6. CrashMonkey project. ACE documentation: sequence lengths count core operations and the input space is bounded.

Sources reviewed 12 October 2026. Historical findings are attributed to their original studies. No current vulnerability claim, hardware test or original empirical failure rate. Source works retain their own rights.