Using Dynamically Layered Definite Releases for Verifying the RefFS File System
Talkat 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) · 2024-07-10..07-12·
summary
RefFS is a concurrent in-memory file system with a machine-checkable proof that guarantees both safety and liveness by enforcing dynamically layered definite releases to prevent circular blocking and handle ad-hoc synchronization and nested waits. The verification is implemented in the MoLi framework (Coq-style proofs over a C model), and the work finds and helps fix a critical deadlock in Linux VFS locking. RefFS runs faster than AtomFS, showing the approach is practical.
AI-written summary · about
chapters (13)
- 0:00File system verification intro
- 1:06File system liveness challenges
- 2:50Deadlocks in file systems
- 4:36Prior verification limits
- 4:57Moly verification framework
- 6:24Unblocking actions layering
- 7:06Moly framework components
- 7:49Moly on RefFS and Linux vFS
- 11:02RefFS design and refcounting
- 11:45Linux vFS locking flaws
- 13:08Locking rules formalization
- 13:28Proof effort and performance
- 14:11Summary and open topics
related talks
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
14mA Refinement Methodology for Distributed Programs in Rust
21mNew Techniques to Improve Small I/O Workloads in Distributed File Systems
58mFrom Formal Verification to Correctly Rounded Math Libraries
17mSingularFS: A Billion-Scale Distributed File System Using a Single Metadata Server
16mLock-Free Collaboration Support for Cloud Storage Services with Operation Inference
14mAutomatically Verifying Replication-aware Linearizability
28mReasoning about Distributed Reconfigurable Systems