SquirrelFS: using the Rust compiler to check file-system crash consistency
Hayley LeBlanc, Nathan Taylor, James Bornholt, Vijay Chidambaram
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了最后一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper4
- Silhouette: Leveraging Consistency Mechanisms to Detect Bugs in Persistent Memory-Based File SystemsBing Jiao, Ashvin Goel, An-I Andy WangFAST 2025 · 被引用 2 次
- Fast and Synchronous Crash Consistency with Metadata Write-Once File SystemYanqi Pan, Wen Xia, Yifeng Zhang, Xiangyu Zou 等OSDI 2025
- Rage Against the State Machine: Type-Stated Hardware Peripherals for Increased Driver CorrectnessTyler Potyondy, Anthony Tarbinian, Leon Schuermann, Eric Mugnier 等ASPLOS 2026
- TickTock: Verified Isolation in a Production Embedded OSVivien Rindisbacher, Evan Johnson, Nico Lehmann, Tyler Potyondy 等SOSP 2025
它引用的顶会 Paper10
- An Empirical Guide to the Behavior and Use of Scalable Persistent MemoryJian Yang, Juno Kim, Morteza Hoseinzadeh, Joseph Izraelevitz 等FAST 2020 · 被引用 470 次
- Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully 等SOSP 2021 · 被引用 63 次
- Storage Systems are Distributed Systems (So Verify Them That Way!)Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell 等OSDI 2020 · 被引用 52 次
- AGAMOTTO: How Persistent is your Persistent Memory Application?Ian Neal, Ben Reeves, Ben Stoler, Andrew Quinn 等OSDI 2020 · 被引用 43 次
- WineFS: a hugepage-aware file system for persistent memory that ages gracefullyRohan Kadekodi, Saurabh Kadekodi, Soujanya Ponnapalli, Harshad Shirwadkar 等SOSP 2021 · 被引用 35 次
相关 Paper
- Chipmunk: Investigating Crash-Consistency in Persistent-Memory File SystemsHayley LeBlanc, Shankara Pailoor, Om Saran K. R. E., Isil Dillig 等EuroSys 2023 · 被引用 11 次
- RedLeaf: Isolation and Communication in a Safe Operating SystemVikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel 等OSDI 2020 · 被引用 86 次
- 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 次
