Applications rely on file systems to store their data, but even carefully written applications and file systems may have bugs that cause data loss, especially in the face of system crashes (e.g., due to power failure).  Even in mature file systems such as Linux ext4, bugs that can lead to data loss are not uncommon.  Application developers also misuse file-system APIs in ways that lead to user data being lost after a crash.

Many of these bugs are subtle: the system works in most cases, but an inopportune combination of system calls and crashes can trigger a bug.  A common approach for dealing with these bugs is to use bug-finding tools, model checking, testing, and so on to find bugs and then fix them.  While these approaches are effective at finding some bugs, they cannot prove the absence of bugs in the resulting systems.

Formal verification is a good way to prove the absence of bugs in a file system.  By considering all possible operations and crashes, verification can ensure that the file system is bug-free.  Our earlier work on FSCQ [Chen et al. 2015] shows that it is possible to build a certified system (i.e., one with a machine-checkable proof that its implementation meets its specification).  However, there is large gap between FSCQ and a practical certified file system, owing to FSCQ's poor performance.

This project explored several techniques to improve performance of storage systems, often requiring a new verification approach:

- Performance: Delayed writes. DFSCQ extends FSCQ with delayed writes. DFSCQ provides a precise specification for fsync and fdatasync, which allow applications to achieve high performance and crash safety.  DFSCQ's specification captures the behavior of sophisticated optimizations, including log-bypass writes, and DFSCQ's proof rules out some of the common bugs in file-system implementations despite the complex optimizations.  An evaluation shows that DFSCQ achieves 103 MB/s on large file writes to an SSD and durably creates small files at a rate of 1,618 files per second.  This is slower than Linux ext4 (which achieves 295 MB/s for large file writes and 4,977 files/s for small file creation) but much faster than two previous verified file systems, Yggdrasil and FSCQ.

- Verification: layered recovery.  Argosy is a framework for machine-checked proofs of storage systems that supports layered recovery implementations with modular proofs.  Reasoning about layered recovery procedures is especially challenging because the system can crash in the middle of a more abstract layer's recovery procedure and must start over with the lowest-level recovery procedure.  Argosy introduces recovery refinement, a set of conditions that ensure proper implementation of an interface with a recovery procedure. Argosy includes a proof that recovery refinements compose, using Kleene algebra for concise definitions and metatheory.  We implemented Crash Hoare Logic, the program logic used by DFSCQ, to prove recovery refinement, and demonstrated the whole system by verifying an example of layered recovery featuring a write-ahead log running on top of a disk replication system.

- Performance: From Haskell to Go. Due to the rigidity of Coq's extraction and the overhead of Haskell, the resulting code’s CPU performance can suffer, with limited opportunity for optimization. To address this challenge, we built Goose, a subset of Go and a translator from that subset to a model in Perennial (see below) with supports for reasoning about Go threads, data structures, and file-system primitives.

- Performance and verification: Concurrency with Perennial.  Perennial is a framework for verifying concurrent, crash-safe systems.  Perennial extends the Iris concurrency framework with three techniques to enable crash-safety reasoning: recovery leases, recovery helping, and versioned memory.  We implemented and verified a crash-safe, concurrent mail server, Mailboat, using Perennial and Goose that achieves speedup on multiple cores.

- Performance and verification: Concurrency with GoJournal and Perennial2.  GoJournal is a verified, concurrent journaling system that provides atomicity for storage applications, together with Perennial 2.0, a framework for formally specifying and verifying concurrent crash-safe systems. GoJournal’s goal is to bring the advantages of journaling for code to specs and proofs.  Perennial 2.0 makes this possible by introducing several techniques to formalize GoJournal’s specification and to manage the complexity in the proof of GoJournal’s implementation. Lifting predicates and crash framing make the specification easy to use for developers, and logically atomic crash specifications allow for modular reasoning in GoJournal, making the proof tractable despite complex concurrency and crash interleavings.  Performance experiments with an unverified NFS file system using GoJournal show similar performance (e.g., 90–95% throughput creating small files on an in-memory disk) to Linux’s NFSserver exporting an ext4 file system, suggesting that GoJournal is a competitive journaling system.

We incorporated ideas from this research in a new class on Principles of Computer Systems (https://6826.csail.mit.edu/2020/), which we taught several times during the lifetime of the project.

Last Modified: 07/01/2021
Modified by: M. Frans Kaashoek