Verifying a high-performance crash-safe file system using a tree specification
Haogang Chen, Tej Chajed, Alexander Konradi, Stephanie F. Wang, Atalay Mert İleri, Adam J. Chlipala, M. Frans Kaashoek, Nickolai Zeldovich · 2017
DFSCQ 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 (2) provides a machine-checked proof that its implementation meets this specification. 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.