Thesis defense: Verifying a concurrent, crash-safe file system with sequential reasoning

The file system is an important service of the operating system, yet implementations still occasionally have bugs that can lead to incorrect results or even data loss. What makes it difficult to write a correct file system is that even simple operations can execute in many ways due to concurrency and power failures, making it challenging to think through or test all possibilities. Formal verification offers a promising solution by using a proof to show the file-system code always meets its specification.

This thesis develops DaisyNFS, a verified, concurrent, and performant file system. The first contribution is new verification foundations for crashes and concurrency that make it possible to reason about high-performance, realistic storage systems at all. The second contribution is the design and implementation of the file system on top. DaisyNFS has a verification-friendly design based on transactions so that most of the code enjoys sequential reasoning. Underlying the file system is a verified, high-performance transaction system with sophisticated concurrency. The overall file system is performant compared to Linux NFS exporting ext4 over a range of benchmarks — at least 75% the throughput with a single client and in-memory disk, and comparable performance when multiple clients are writing concurrently.