SquirrelFS: using the Rust compiler to check file-system crash consistency

TL;DR

This paper tackles crash consistency for file systems on persistent memory by combining Rust's typestate programming with a new crash mechanism called Synchronous Soft Updates (SSU). The central idea is to statically encode and enforce the correct ordering of metadata updates at compile time, avoiding heavy proofs while providing verifiable guarantees. The authors implement SquirrelFS in Rust, demonstrate compilation-based crash-consistency checks, and validate performance against state-of-the-art PM file systems, showing comparable or better results across micro- and macro-benchmarks. The work also includes Alloy-based model checking and a detailed development experience, highlighting both the benefits and limitations of a typestate-driven approach for crash safety with potential applicability beyond PM environments.

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.

Figures (5)

• Figure 1: For a soft updates file system to be crash-consistent, directory entries should only point to fully-initialized, durable inodes. In existing file systems, all persistent inodes have the same type, regardless of whether they are durable or have been initialized. With typestate, durability and the inode's contents are reflected in its type.
• Figure 2: The figure shows the steps in atomic soft updates rename. The dotted lines represent rename pointers and the solid lines represent inode pointers. src and dst are directory entries. The labels "v" and "i" indicate whether a directory entry is valid or invalid.
• Figure 3: The figure shows the persistent updates and corresponding dependencies made during mkdir. Inodes are dark gray and directory entries are white. Each object is labeled with its operational typestate and its outline indicates whether it is clean (solid) or dirty (dotted).
• Figure 4: The figure shows the main components of SquirrelFS. Each CPU has its own pool of pages and private page allocator. The inode allocator is shared between all CPUs. Volatile indexes are stored in VFS data structures.
• Figure 5: This figure shows the performance of the evaluated file systems on different benchmarks and applications. (a) shows absolute latency of different file system operations; (b), (c), and (d) show the relative throughput in kops/s of each system relative to Ext4-DAX on filebench, YCSB on RocksDB, and LMDB respectively.