Specifying and Checking File System Crash-Consistency Models
Specifying and Checking File System Crash-Consistency Models
复制标题
DOI：
10.1145/2954679.2872406
复制
发表时间：
2016-04-01
影响因子：
--
通讯作者：
Wang, Xi
中科院分区：
文献类型：
--
作者：
Bornholt, James;Kaufmann, Antoine;Wang, Xi
应用程序依赖于持久存储来在系统崩溃后恢复状态。但是POSIX文件系统接口没有定义崩溃的可能结果。因此，它是很难为应用程序的作家正确理解的顺序和文件系统操作之间的依赖关系，这可能会导致损坏的应用程序状态，在最坏的情况下，灾难性的数据loss.This本文提出了崩溃一致性模型，类似于内存一致性模型，它描述了跨崩溃的文件系统的行为。崩溃一致性模型包括两个石蕊测试，证明允许和禁止的行为，公理和操作规范。我们提出了一个正式的框架，用于开发崩溃一致性模型，和一个工具包，称为FERRITE，用于验证这些模型对真实的文件系统实现。我们为ext4开发了一个崩溃一致性模型，并使用FERRITE来演示ext4实现的不直观的崩溃行为。为了向应用程序编写者展示崩溃一致性模型的实用性，我们使用我们的模型来原型化概念验证和合成工具，以及用于崩溃安全应用程序的新库接口。
Applications depend on persistent storage to recover state after system crashes. But the POSIX file system interfaces do not define the possible outcomes of a crash. As a result, it is difficult for application writers to correctly understand the ordering of and dependencies between file system operations, which can lead to corrupt application state and, in the worst case, catastrophic data loss.This paper presents crash-consistency models, analogous to memory consistency models, which describe the behavior of a file system across crashes. Crash-consistency models include both litmus tests, which demonstrate allowed and forbidden behaviors, and axiomatic and operational specifications. We present a formal framework for developing crash-consistency models, and a toolkit, called FERRITE, for validating those models against real file system implementations. We develop a crash-consistency model for ext4, and use FERRITE to demonstrate unintuitive crash behaviors of the ext4 implementation. To demonstrate the utility of crash consistency models to application writers, we use our models to prototype proof-of-concept verification and synthesis tools, as well as new library interfaces for crash-safe applications.