Verifying a Concurrent File System with Sequential Reasoning

Explore the development of DaisyNFS, a verified concurrent file system, in this conference talk from ACM SIGPLAN. Dive into the innovative approach of combining interactive proofs in Coq and automated proofs in Dafny to tackle the challenges of crash safety and concurrency in systems software. Learn about the GoTxn transaction system and its verification using the Perennial program logic built on Iris in Coq. Discover how the file-system logic is implemented as atomic transactions, enabling verification through Dafny. Gain insights into the resulting NFS protocol server implementation, which achieves good performance while maintaining a low proof burden for file-system logic. Understand the importance of verified systems in preventing bugs that can lead to security vulnerabilities and data loss in critical software infrastructure.

[Dafny'24] Verifying a concurrent file system with sequential reasoning