Verifying Crash Consistency with Fault Injection

A crash-consistency claim is a universal statement: for every write the device could have lost, and every order it could have applied the survivors in, the recovered state is one the reader can interpret. A test that cuts power at one moment exercises one point in that space. Running it a thousand times exercises a thousand points, chosen by timing rather than by structure, and the points that matter are often the ones a timing-driven test never lands on. Verifying the claim means enumerating the states the device permits, and that enumeration is a property of the program’s write sequence rather than of the wall clock.

The failure model has to be stated before it can be tested

The device model determines the state space, and different models give different answers about the same code. The simplest model is that every write either happens or does not, and the set of surviving writes is arbitrary. That model is wrong for a device with a cache and correct for a device that writes through, so a test built on it will report failures that cannot occur and miss ones that can.

A more accurate model for a cached device has three parameters: which writes have been acknowledged, which of the acknowledged ones have reached media, and in what order. The acknowledgement boundary is what a flush or a forced unit access establishes, and the model’s central rule is that a write acknowledged after a flush is ordered after every write the flush covered. A write acknowledged without a barrier carries no ordering at all relative to any other write. That single rule generates the interesting states, because it is the only thing that constrains the permutations.

Torn writes are a separate axis. A write of more than one sector can land partially, and the model has to allow a prefix of the sectors, a suffix, or an arbitrary subset if the device’s internal read-modify-write is not atomic. Restricting the model to whole-write granularity makes the state space smaller and the test tractable, and it also makes the test unsound for the metadata blocks that are larger than a sector, which on a filesystem with 4 KiB blocks is all of them.

Enumerating the states a write sequence permits

The enumeration is mechanical once the sequence is known. Record every write the program issues, in order, with the barrier that follows it. Then generate the set of media states by choosing, for each barrier-delimited group, a subset of the group’s writes to have survived, and by choosing an order within each group. A program with ten writes and three barriers has a state space that is large but finite, and most of it collapses because many subsets produce the same recovered state.

The collapse is what makes the method practical. Two media states that differ only in the order of two writes to disjoint regions recover identically, so the enumeration can canonicalize them. Two states that differ in whether a commit record survived are genuinely different and both must be checked. A tool that does this well reports the distinct recovered states rather than the raw permutations, and the count is usually in the hundreds for a filesystem operation rather than in the millions.

/* A harness records the write sequence and replays it into a shadow media. */
struct op { uint64_t off; size_t len; const void *data; int barrier_after; };
static struct op ops[4096];
static size_t nops;

static void record_write(uint64_t off, size_t len, const void *p)
{
    ops[nops++] = (struct op){ off, len, p, 0 };
}
static void record_barrier(void) { ops[nops - 1].barrier_after = 1; }

The harness has to observe the writes at the syscall or block-layer boundary rather than at the application’s logical operations, because the mapping from one logical operation to many writes is exactly where the ordering bugs live. A single rename may become a directory block write, an inode write, and a bitmap update, in an order the application did not choose and cannot see. The same reduction appears in the protocol described in What fsync Actually Waits For, where one logical publication becomes three separate objects that must reach media in a fixed order.

Checking a recovered state needs an invariant, not a golden image

A recovered state cannot be compared against a golden image, because the correct answer depends on which writes survived. A crash after the data write but before the commit legitimately recovers to the old state; a crash after the commit legitimately recovers to the new one. Comparing against either alone produces false failures.

What the check needs is an invariant that holds in every permitted state. For a filesystem, that is the structural invariant: every reachable block is allocated, no block is allocated twice, every directory entry names an inode whose link count matches the number of entries, the free-space map agrees with the set of unreferenced blocks. For an application, it is the semantic invariant: the counter on page 10 and the total on page 40 are consistent, the log’s tail is at or before its head, the checkpoint’s root points to blocks that exist. The last of those is the invariant that shadow paging is built to preserve, and it is the one a publication protocol can break while every individual block still checksums correctly.

The invariant is where the real work sits, because it has to be strong enough to catch the bug and weak enough to accept every legal state. An invariant that demands the new state rejects legal recoveries; one that accepts anything checks nothing. The usual formulation is a set of predicates that a recovered state must satisfy, each derived from a specific way the code could be wrong: a pointer written before its target, a commit record before its data, a free before its last reference.

Recovery must itself be tested

The recovery procedure runs on a state produced by a crash, and it can crash in turn. A recovery that is interrupted after applying half the log produces a state that the enumeration must also include, and the invariant must hold there too. This is the reason replay has to be idempotent, and it is a property that is easy to lose: a recovery that increments a counter, or that appends a record to a log rather than rewriting a page, is not idempotent, and a second crash during recovery produces a state no first crash could have.

Testing this means applying the same enumeration to the recovery code’s own write sequence, starting from each recovered state. The state space multiplies, and in practice the second level is sampled rather than enumerated, with the sample chosen to include the writes that recovery issues at each step. The failures found this way are disproportionately severe, because they occur exactly when the system is already in a degraded state and the operator’s next action is usually to try again.

The invariant also has to be checked after recovery, not only before. A recovery procedure can turn a legal state into an illegal one, by truncating a file to a length the metadata does not support or by clearing a bitmap entry for a block that is still referenced, and the pre-recovery invariant will not catch it. The post-recovery check is the one that corresponds to what the next boot will see.

What the method cannot find

The enumeration assumes the device behaves as modeled. A device that acknowledges a write it did not perform, that reorders a flush behind a write, or that corrupts a block silently is outside the model, and a test built on the model will pass on such a device. Detecting that class requires end-to-end verification, reading back and comparing, which is a different kind of test with a different cost, and it can only be done against the actual hardware or its emulation.

The enumeration also assumes the program’s write sequence is deterministic. A program whose writes depend on timing, on thread scheduling, or on the contents of a cache has a different sequence on every run, and the harness records one of them. Covering the others means running the enumeration over many recorded sequences, which is sampling again, with the same weakness: the sequences that matter are the ones the recorder did not happen to produce.

There is a further limit that no test addresses: the model is only as good as the specification behind it. A filesystem that assumes a device honors a flush, tested against an emulator that honors it, is verified against an assumption rather than against the hardware. The gap between the two is where real failures live, and closing it requires either hardware that documents its behavior or a redundancy scheme that tolerates the behavior being wrong. That is why checksums and repair are part of the durability story rather than an admission of defeat, as described in Torn Writes and the RAID Write Hole.

The claim, stated honestly

A verified system is one whose permitted post-crash states have been enumerated, whose invariant has been checked in each, and whose recovery has been shown to preserve the invariant when interrupted. That is a stronger statement than “it passes the crash tests”, and it is a weaker statement than “it is correct”, because it is conditional on the device model and on the completeness of the invariant.

Stating the claim that way is useful precisely because it names the assumptions. A system whose claim is “every state permitted by a device that honors flush and FUA satisfies the structural invariant” tells a reader exactly what to check about the device and exactly what the recovery guarantees. A system whose claim is “crash-safe” tells a reader nothing, and the difference between the two is the difference between an argument and a slogan. The mechanisms described throughout this cluster, the persistence domain, the barrier, the log, and the shadow root, are the terms in which such an argument is written; the enumeration is what turns the argument into evidence.