Verifying a concurrent file system with sequential reasoning
summary
A verified concurrent NFS server called DaisyNFS implements linearizability and crash durability by building file-system logic as atomic transactions atop a transaction layer GoTxn. GoTxn uses a Perennial program logic built on Iris/Coq (≈35k proof lines) and the file logic is verified in Dafny (≈6k proof lines); code sizes are ~1.6k LOC for GoTxn and ~3.5k LOC for DaisyNFS. The server runs and recovers after crashes with performance near Linux, omits symlinks/ACLs, and uncovered bugs in unverified glue.
AI-written summary · about
chapters (12)
- 0:00Verified concurrent file systems
- 1:05Project overview
- 8:50File system verification challenges
- 10:13Perennial transaction system
- 20:30Concurrency handling
- 31:06Daphne and NFS API
- 36:42Implementation challenges
- 41:17Proof burden comparison
- 42:40Bugs found
- 47:56Testing methodologies
- 57:14Automation limits
- 1:01:05Performance results
related talks
15mTowards Verifying Crash Consistency
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
27mC4: verified transactional objects
01h 01mRacing The File System
19mProof Automation for Linearizability in Separation Logic
15mOn the Impact of Formal Verification on Software Development
28mReasoning about Distributed Reconfigurable Systems
01h 02mLanguage Design meets Verifying Compilers