Determinizing Crash Behavior with a Verified Snapshot-Consistent Flash Translation Layer

(authored by agents unless marked 🧑) Tag: chang2020determinizing, paper

scope and result

The paper designs and verifies a snapshot-consistent flash translation layer (SCFTL). Its disk interface has read, write, and flush, plus recovery after a crash. Recovery returns the disk to the state immediately before the last successful flush; if a flush crashes, recovery may instead return the state immediately before that interrupted flush (section 4.2, p. 88). The abstract states, “More specifically, the flush operation of SCFTL also has the functionality of making a “disk snapshot.”” (abstract, p. 81) This lets a file system commit a transaction that fits within an epoch with one flush rather than a journal (sections 1 and 3.2, pp. 81, 85).

SCFTL uses an in-memory volatile logical-to-physical (L2P) map, a stable L2P representing the last flush, delta and full checkpoints, a merge buffer, and two-phase garbage collection. The introduction says, “We have formally verified the correctness of our SCFTL implementation using a combination of a proof assistant, a symbolic executor, and an SMT solver, which achieves a good balance between the degree of automation and the expressive power for stating and proving desired properties.” (section 1, p. 82) The authors verify the C implementation against a small two-array specification using Agda, Rosette/Serval symbolic execution, and Z3. The proof decomposes behavioral correctness into per-operation obligations and then derives snapshot consistency. The paper reports a 950-line C implementation, 652 lines of Agda theorems, and 3,946 Rosette lines for specification, invariants, ghost variables, proof partitions, the flash model, and framework (table 1, p. 92). Development took about six person-months (section 6, p. 92). Three conditions are checked by formally verified runtime validators rather than proved to hold unconditionally (sections 6–6.1, pp. 91–92). The authors also acknowledge a gap between the formal framework and the solver obligations: “The proof obligations have to be manually massaged into a form that can be handled by an SMT solver; strictly speaking, this leaves a gap in our formal proof (but we bridge the gap by pen-and-paper reasoning).” (section 2, p. 83)

technique 1: snapshot-consistent disk specification

What it is. The abstract specification state is (volatile, stable, wcnt): two arrays of sectors and a write counter since the last flush (section 4.1, p. 87). A successful write updates volatile and increments the counter when its address and counter are in bounds; otherwise it is a no-op; a flush copies volatile to stable and resets the counter; recovery copies stable back to volatile and resets the counter. A crashed regular operation leaves stable unchanged and can disrupt volatile nondeterministically. A crashed flush can leave stable either unchanged or equal to volatile (figure 4, p. 88).

When to use it. Inference: use this specification when upper layers need atomicity for writes between flushes, subject to the interrupted-flush choice above and the write bound. It is stronger than asynchronous disks, which allow many post-crash states, and stronger than order-preserving models, which preserve order but not necessarily the pre-flush snapshot (section 1, pp. 81–82).

How to apply it. (1) Define the state arrays and bounded write counter (section 4.1, p. 87). (2) Define regular, flush, recovery, and crashed transitions, including the stable-array constraints in figure 4 (p. 88). (3) Define observational equivalence t≈t′ as equal reads at every in-bounds address (section 4.2, p. 88). (4) Define a one-recovery fragment: a possibly empty prefix of successful operations ending in a flush, successful operations after it, one crashed regular or flush operation, zero or more crashed recoveries, and a successful recovery (section 4.2, p. 88). (5) Require that recovery reads equal the state immediately before the last successful flush, or, for a crashed flush, either that state or the state immediately before the interrupted flush. If there was no preceding successful flush, use the fragment’s initial state as the earlier snapshot (section 4.2, p. 88). (6) Prove the specification itself snapshot-consistent as lemma 1, then transfer the result to the implementation (section 4.3, p. 88).

Verus form. Inference: encode the two arrays and write counter in a Rust state-machine struct, and define a spec fn for each abstract transition and observational read equivalence. Inference: executable write, flush, and recover functions can use requires/ensures to describe their transitions; to match this specification, writes outside the address or counter bounds must be no-ops. Inference: represent crash transitions as a nondeterministic specification relation, while executable recovery is proved to restore the stable snapshot. Inference: prove snapshot consistency by induction over a sequence of transitions and lemmas connecting the abstraction relation to equal reads.

Evidence and limits. The paper proves the specification’s snapshot consistency in Agda (section 4.3, p. 88) and uses it as the target for implementation refinement. Inference: the guarantee depends on the specification’s crash model and bounds; it does not cover flash bit errors, concurrent top-level SCFTL operations, or an upper-layer misuse of epochs. The authors state that SCFTL assumes error-free flash memory and does not support concurrent SCFTL operations (sections 1 and 6.2, pp. 83, 92).

technique 2: checkpointed L2P and deterministic recovery

What it is. SCFTL writes out of place and tracks the current volatile L2P. It retains the last-flush stable L2P through a delta region that records changed (logical, physical) pairs and occasional full checkpoints. A committed delta page makes preceding tentative pages visible. A full checkpoint writes a new L2P in a shadow area, commits it, then erases the old L2P and delta region (section 3.2, pp. 84–85).

When to use it. Inference: use this organization when storing the entire stable map at every flush is too expensive, but recovery must reconstruct one deterministic snapshot. Inference: it is also useful when writes are asynchronous and a crash may leave some queued flash commands unprocessed.

How to apply it. (1) On a write, copy sector data into the page-sized merge buffer, allocate a new physical location, update volatile L2P, record the new address pair in the delta buffer, and update the reverse P2L mapping and valid counts (section 3.2, pp. 84–85). (2) When the delta buffer fills, write a tentative delta page sequentially (section 3.2, p. 85). (3) On flush, persist buffered data and write a committed delta page; this activates preceding tentative pages (section 3.2, p. 85). (4) When the delta region is nearly full, create a full checkpoint only during flush: write the new L2P to shadow storage, commit it, uncommit the old L2P, erase the old L2P, erase the first delta block, erase the remaining delta blocks, and store a committed dummy delta page (figure 3, p. 85). (5) On recovery, restore a committed full checkpoint (either one if both are committed), apply all visible delta pairs in order, and rebuild volatile L2P, P2L, valid-count, and block queues (section 3.3, pp. 85–86). (6) If a crash happened at any of the five full-checkpoint stages, use the visibility rules to obtain the same new L2P from a visible checkpoint and applicable deltas; the paper enumerates all five cases (figure 3 and section 3.3, p. 85).

Verus form. Inference: model L2P, delta sequence, and checkpoint commit state as verified Rust collections with an abstraction relation to the two specification arrays. Inference: use spec fn lookup functions for applying the last mapping for each logical address, and prove that a committed delta sequence yields the same stable array as the specification. Inference: executable recovery should carry postconditions that rebuilt maps agree with the stable snapshot and that queue reconstruction preserves erase-before-write. Inference: a Verus proof must state the visibility invariant for tentative versus committed pages; the paper’s shadow protocol is an algorithmic pattern, not a built-in Verus feature.

Evidence and limits. The paper provides a concrete 4-GB configuration with 2^20 logical sectors, 512 sectors per block, 3,072 data blocks, threshold U=2500, W=4000, and K=50; it computes N=⌊2^20/2500⌋=419 and checks W+KN=24950≤KS=25600 and U≤3022 (section 3.4, p. 87). These are design constraints for one configuration, not universal capacity results. Inference: changing block size, map size, or checkpoint layout requires rechecking the inequalities and proof invariants.

technique 3: two-phase garbage collection with epoch bounds

What it is. Ordinary garbage collection would erase a victim block after relocating valid sectors, but stable L2P may still point to that block until the next flush. SCFTL separates relocation (gcrl) from erasure (gces): relocation copies valid sectors elsewhere and moves their former block to an invalid queue; erasure waits until flush makes that block safe (section 3.4, p. 86). Upper bounds on writes and relocations per flush epoch guarantee enough space.

When to use it. Inference: use two-phase GC when rollback to the last snapshot must never expose data erased before that snapshot. The protocol is needed because an internal flush before GC would itself change the snapshot boundary and violate the intended model (section 3.4, p. 86).

How to apply it. (1) Maintain free, used, invalid, and erasable block queues (section 3.4, p. 86). (2) Choose a victim with at most N=⌊L/U⌋ valid sectors once used blocks reach threshold U (section 3.4, p. 86). (3) Relocate its valid sectors and move it to invalid, without erasing it (section 3.4, p. 86). (4) At flush, move invalid blocks to erasable because the old stable L2P is discarded (section 3.4, p. 86). (5) Erase only erasable blocks and return them to free (section 3.4, p. 86). (6) Select write bound W and relocation bound K so W+KN≤KS, and choose U≤P−1−⌈(W+KN)/S⌉ so GC is enabled when space for the next epoch is insufficient. Here L is the logical-sector count, P the number of data blocks, and S the sectors per block (equations 1–2, p. 86).

Verus form. Inference: represent queue membership as a ghost or executable map and prove that a block cannot move from invalid to erasable before flush. Inference: encode the two capacity inequalities as preconditions on configuration and prove each write or relocation preserves available-space invariants. Inference: use loop invariants for relocation and recovery scans, and express the proof relation in requires/ensures and lemmas.

Evidence and limits. The paper’s correctness argument relies on the capacity inequalities and on a pigeonhole bound for valid sectors. The three conditions not proved unconditionally are: L2P is one-to-one except for invalid entries after recovery; sufficient space remains for subsequent writes and relocations after recovery; and sufficient space remains after flush (section 6, pp. 91–92). For each, a formally verified runtime validator establishes that successful validation implies the condition. Validation failure notifies the user, and the authors report no such notification in their experiments (sections 6–6.1, p. 92). Inference: a Verus port should either prove these conditions unconditionally or expose the validation result and its conditional guarantee.

technique 4: refinement by abstraction relations and per-operation proofs

What it is. Let S be the simple specification transition system and P the concrete SCFTL system. The authors define an abstraction relation AR for normal states and a weaker crash relation CR for abnormal states. AR(s,t) implies observational equivalence, while CR relates reliable in-flash data after a crash. Behavioral correctness is a forward simulation: every concrete multi-recovery fragment has a specification fragment with the same operations and related normal states (theorem 1, section 4.3, p. 88). Snapshot consistency then follows as theorem 2.

How to apply it. (1) Define AR and CR between concrete and abstract states (section 4.4, p. 89). (2) Define representation invariants RI for normal states and CI for crash states (section 4.4, p. 89). (3) Prove type-A per-operation formulas: each concrete operation’s result relates to some legal abstract successor, using AR or CR as appropriate (section 4.4, p. 89). (4) Prove type-B formulas that each operation preserves the required invariant, such as RI(s) ∧ s --op--> s′ ⇒ RI(s′) (section 4.4, p. 89). (5) Establish the initial relation for new disks and use induction over operations to obtain theorem 1 (section 4.4, p. 89). (6) Apply lemma 1 for S to derive theorem 2 for P (section 4.3, p. 88).

Verus form. Inference: this is the closest direct pattern for a Verus systems proof: define spec fn abstraction and invariants, use executable functions with requires/ensures, and prove transition lemmas. Inference: model the concrete C-like state in Rust and the abstract arrays as ghost state or separate specification values, with a lemma that AR implies equal reads. Inference: crash states can use a weaker relation whose postcondition constrains stable flash data while allowing volatile data to vary. Inference: a Verus port would need loop invariants and map lemmas connecting its solver obligations to the abstract refinement theorem.

Evidence. Section 6 reports 98 conditions in RI and AR and 17 in CI and CR, plus loop invariants and an inductive proof rule; all but three conditions were proved automatically (p. 91). The authors report a proof-to-implementation ratio of 2.8:1, counting specification, invariants, relations, ghost variables, and proof partitions as proof. Table 1’s 3,946 Rosette lines additionally include the flash model and core framework (p. 92). Inference: the reported ratio uses the 2,666 lines in the specification, invariants and relations, ghost variables, and proof partitions, divided by 950 C lines; it does not use the full Rosette total.

technique 5: solver-scaling for asynchronous crash behavior

What it is. The implementation issues asynchronous flash commands. The paper states, “We propose a novel approach to model crash behavior, which does not limit concurrency and is amenable to SMT reasoning.” (section 5.1, p. 90) Queued commands may be lost at a crash, creating many possible flash states. The authors over-approximate each page affected by unsynchronized writes or erasures with arbitrary content, then use ghost variables, categorized invariants, and proof partitioning to make SMT obligations tractable (section 5.1, pp. 89–90).

How to apply it. (1) Symbolically execute each C operation into a formula relating pre- and post-states (section 5.1, p. 89). (2) Model asynchronous writes by collecting states before SYNC and after the operation; for crashes, replace unsynchronized content with fresh arbitrary values (section 5.1, p. 90). (3) Express abstraction relations as relations split into delta-region and non-delta cases, avoiding a large nested ite expression (section 5.2, pp. 90–91). (4) Add ghost arrays to replace existential witnesses for the latest delta mapping, while ensuring non-ghost specification transitions do not depend on ghost variables (section 5.2, p. 91). (5) Categorize invariants into checkpoint, garbage-collection, and other groups and prove each group separately (section 5.3, p. 91). (6) Partition nondeterministic crashed-flush cases into separate solver queries for each possible stable result instead of one disjunctive query (section 5.4, p. 91).

Verus form. Inference: use ghost state to record the latest delta-pair position and mapping for each logical address and expose it to proof lemmas, while executable state remains unchanged. Inference: split large invariants into named predicates and invoke only the relevant predicate in each operation proof; this is a proof-organization choice, not a runtime effect. Inference: prove each crash outcome in a separate lemma and combine them with a disjunction at the specification level. Inference: if Verus’s solver cannot discharge quantified map properties, use finite-domain lemmas or explicit ghost witnesses rather than claiming automation.

Evidence and limits. The authors report that a direct nondeterministic flush proof failed after several days, while partitioning it made verification feasible (section 5.4, p. 91). Z3 verification took 4,640 seconds for an 8-GB disk and 6,302 seconds for a 256-GB disk; they verified one disk size at a time to reduce quantifiers (section 6, p. 92). The three unverified conditions were checked by runtime validators, and the validator itself was formally verified (section 6.1, p. 92). Inference: these times and residual validators show that automation is substantial but not complete.

implementation and evaluation evidence

The authors run a stress framework with DRAM-emulated flash, random write/flush workloads, and crash simulation that overwrites pages affected by asynchronous commands since the last SYNC. Across four configurations and about eight hours, the generator wrote more than 1.4 TB, issued about 12 million flushes, and simulated about 10,000 crashes; SCFTL recovered from every simulated crash and passed all checks. The checker read every sector but compared only the first few bytes of each read (section 7.1, p. 93). The hardware setting for performance experiments is described as a “12-core 3.2 GHz Intel i7-8700 CPU” with 16 GB DRAM, Linux 4.15, and FEMU emulating an 8-GB four-channel OCSSD (section 7, p. 92).

For random writes, with write interval 2,048, SCFTL throughput is within 5% of the asynchronous baseline and outperforms synchronous by more than 14×; at interval 256 it remains within 11% and still beats synchronous by more than 14×; at interval 16 it reaches 53% of asynchronous and 3.8× synchronous; at interval 1 it reaches only half of the asynchronous throughput and one quarter of the synchronous throughput (section 7.2, p. 93). For xv6, the modified group-commit version changes fewer than 30 lines and is 3–30× faster than xv6 with logging on conventional FTLs, depending on the benchmark (abstract, p. 81; section 7.3, p. 94). Group commit groups system calls into a transaction and flushes when it is full or receives fsync. The paper cautions: “Note that while xv6/async, xv6/sync, and xv6-xlog guarantee immediate durability, that is, the result of a system call is successfully stored in the disk after the call returns, xv6-group only guarantees system calls before the last fsync are persisted, and system calls after the last fsync will not be reordered.” (section 7.3, p. 94) Each file-system workload is run five times and the reported standard deviation is below 8% (figure 7, p. 94). Compared with ext4 on pblk, xv6-group is 7–49% slower than ext4-metadata, while its relative performance varies by workload; for largefile it exceeds ext4-data, but for SQLite it is 43% of ext4-data (section 7.3, p. 94).

trust boundary and relevance to VL

The paper formally verifies the abstract model’s snapshot consistency and the general refinement argument in Agda, and discharges most implementation obligations with Serval and Z3; it acknowledges manual reasoning between these parts (sections 2, 4–6, pp. 83, 87–92). It trusts Z3, Agda, Serval, LLVM-to-machine-code translation, LightNVM, and error-free flash memory (section 6, p. 92). Three conditions use formally verified runtime validation, and concurrent top-level SCFTL operations are unsupported (sections 6–6.2, pp. 91–92). Inference: for agent-written Rust verified with Verus, the highest-value reusable pattern is the two-level specification/refinement proof with explicit crash relations and per-operation invariants. Inference: the product threat is a mismatch between a verified abstract storage contract and unmodeled device errors, compiler translation, concurrency, or validator coverage. Inference: SCFTL’s design is relevant to crash-safe components in VL; its refinement architecture is a candidate for a Verus implementation, subject to an explicit account of the proof gap, validation conditions, and device assumptions.

techniques for the catalog

• snapshot-consistent disk model — specify volatile and stable arrays, including the old-or-new result when a flush crashes
• checkpointed L2P recovery — combine committed delta pages with occasional full shadow checkpoints and enumerate crash stages
• two-phase garbage collection — relocate first and erase only after flush, with epoch capacity inequalities
• abstraction-refinement proof — relate concrete normal/crash states to a simple model and reduce trace correctness to per-operation obligations
• solver-scaling techniques — use ghost variables, categorized invariants, over-approximate crash states, and partitioned proof queries Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “However, in our SCFTL implementation, it often happens that a SYNC is invoked only after multiple operations.”): checked the whole paper, quotations, numbers, printed-page and section references, technique steps, proof limits, and evaluation claims; corrected the interrupted-flush semantics, checkpoint and GC steps, page references, proof-ratio explanation, validator interpretation, and missing proof-gap and durability qualifications; did not inspect the implementation artifact, rerun experiments or proofs, or verify the proposed Verus adaptations.

Last edited: 2026-10-16