Using the metadata-prefix specification to verify a high-performance crash-safe file system

Haogang Chen, Alex Konradi, Stephanie Wang, Tej Chajed, Atalay Ileri, Adam Chlipala, Frans Kaashoek, Nickolai Zeldovich. Using the metadata-prefix specification to verify a high-performance crash-safe file system. Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP'17). October 2017.

Coming soon!

VDFS is the first file system that (1) provides a precise specification for fsync and fdatasync, which allow applications to achieve high performance and crash safety, and that (2) provides a machine-checked proof that its implementation meets this precise specification. VDFS's proof rules out some of the most common bugs in file-system implementations, as system calls are proved to expose the expected atomic behavior. VDFS's specification also allows applications to prove their own crash safety, avoiding application-level bugs such as forgetting to invoke fsync on both the file and the containing directory.

The key challenge in building VDFS is to write concise specifications for the file system and its internal implementation. VDFS introduces a metadata-prefix specification that captures the properties of fsync and fdatasync, which roughly follows the behavior of Linux ext4. This specification uses a notion of tree sequences -- a logical sequence of file system tree states -- to succinctly describe the possible states after a crash, and to describe how data writes can be re-ordered with respect to metadata updates.

An evaluation shows that VDFS 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. In comparison, Linux ext4 achieves 295 MB/s for large file writes and 4,977 files/s for small file creation. VDFS is much faster than any previous verified file system (none can even implement large file writes, and the fastest can create 350 files/s).