SquirrelFS: using the Rust compiler to check file-system crash consistency
Hayley LeBlanc, Nathan Taylor, James Bornholt, Vijay Chidambaram
Abstract
This work introduces a new approach to building crash-safe file systems for persistent memory. We exploit the fact that Rust’s typestate pattern allows compile-time enforcement of a specific order of operations. We introduce a novel crash-consistency mechanism, Synchronous Soft Updates, that boils down crash safety to enforcing ordering among updates to file-system metadata. We employ this approach to build SquirrelFS, a new file system with crash-consistency guarantees that are checked at compile time. SquirrelFS avoids the need for separate proofs, instead incorporating correctness guarantees into the typestate itself. Compiling SquirrelFS only takes tens of seconds; successful compilation indicates crash consistency, while an error provides a starting point for fixing the bug. We evaluate SquirrelFS against state-of-the-art file systems such as NOVA and WineFS, and find that SquirrelFS achieves similar or better performance on a wide range of benchmarks and applications.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 9083bd4d-e258-4078-aec9-9d4abae39634Cited by top-tier papers4
- Silhouette: Leveraging Consistency Mechanisms to Detect Bugs in Persistent Memory-Based File SystemsBing Jiao, Ashvin Goel, An-I Andy WangFAST 2025 · 2 citations
- Fast and Synchronous Crash Consistency with Metadata Write-Once File SystemYanqi Pan, Wen Xia, Yifeng Zhang, Xiangyu Zou et al.OSDI 2025
- Rage Against the State Machine: Type-Stated Hardware Peripherals for Increased Driver CorrectnessTyler Potyondy, Anthony Tarbinian, Leon Schuermann, Eric Mugnier et al.ASPLOS 2026
- TickTock: Verified Isolation in a Production Embedded OSVivien Rindisbacher, Evan Johnson, Nico Lehmann, Tyler Potyondy et al.SOSP 2025
Builds on10
- An Empirical Guide to the Behavior and Use of Scalable Persistent MemoryJian Yang, Juno Kim, Morteza Hoseinzadeh, Joseph Izraelevitz et al.FAST 2020 · 470 citations
- Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully et al.SOSP 2021 · 63 citations
- Storage Systems are Distributed Systems (So Verify Them That Way!)Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell et al.OSDI 2020 · 52 citations
- AGAMOTTO: How Persistent is your Persistent Memory Application?Ian Neal, Ben Reeves, Ben Stoler, Andrew Quinn et al.OSDI 2020 · 43 citations
- WineFS: a hugepage-aware file system for persistent memory that ages gracefullyRohan Kadekodi, Saurabh Kadekodi, Soujanya Ponnapalli, Harshad Shirwadkar et al.SOSP 2021 · 35 citations
Related papers
- Chipmunk: Investigating Crash-Consistency in Persistent-Memory File SystemsHayley LeBlanc, Shankara Pailoor, Om Saran K. R. E., Isil Dillig et al.EuroSys 2023 · 11 citations
- RedLeaf: Isolation and Communication in a Safe Operating SystemVikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel et al.OSDI 2020 · 86 citations
- Towards Verifying Crash ConsistencyKeonho Lee, Conan Truong, Brian DemskyOOPSLA 2025
- Vinter: Automatic Non-Volatile Memory Crash Consistency Testing for Full SystemsSamuel Kalbfleisch, Lukas Werling, Frank BellosaUSENIX ATC 2022
- NobLSM: an LSM-tree with non-blocking writes for SSDsHaoran Dang, Chongnan Ye, Yanpeng Hu, Chundong WangDAC 2022 · 5 citations
