Model-Checking Support for File System Development
Model-Checking Support for File System Development
复制标题
文件系统开发的模型检查支持
DOI：
10.1145/3465332.3470878
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Kuenning, Geoff
中科院分区：
文献类型：
--
作者：
Su, Wei;Liu, Yifei;Ganesan, Gomathi;Holzmann, Gerard;Smolka, Scott;Zadok, Erez;Kuenning, Geoff
开发和维护文件系统非常耗时，通常需要数年的努力。开发人员经常使用手写的回归套件来测试与api（如POSIX）的遵从性，可惜，这些回归套件只检查文件系统状态空间的一小部分。相反，正式的模型检查可以有效地探索大量的状态空间，从而增加对文件系统实现的信心。然而，模型检查目前还不是文件系统开发的一部分。我们的立场是，文件系统应该预先设计，以方便模型检查。为此，我们介绍了一种高效、全面的文件系统模型检查体系结构MCFS。MCFS依赖于两个新的api来保存和恢复文件系统的内存和磁盘状态。我们描述了早期对文件系统进行模型检查的尝试，包括不成功的或低效的尝试。这些尝试引导我们开发了VeriFS，它实现了新的api。我们用VeriFS来说明MCFS的模型检查原则，VeriFS是一个基于fuse的文件系统，我们能够在MCFS的帮助下快速开发。
Developing and maintaining a file system is time-consuming, typically requiring years of effort. Developers often test compliance with APIs such as POSIX with hand-written regression suites that, alas, examine only a fraction of a file system's state space. Conversely, formal model checking can explore vast state spaces efficiently, increasing confidence in the file system's implementation. Yet model checking is not currently part of file system development. Our position is that file systems should be designed a priori to facilitate model checking. To this end, we introduce MCFS, an architecture for efficient and comprehensive file-system model checking. MCFS relies on two new APIs that save and restore a file system's in-memory and on-disk state. We describe our earlier attempts at model-checking file systems, including unsuccessful or inefficient ones. Those attempts led us to develop VeriFS, which implements the new APIs. We illustrate MCFS's model-checking principles with VeriFS, a FUSE-based file system we were able to quickly develop with MCFS's help.
登录
查看更多内容
通过崩溃优化对文件系统进行一键式验证
DOI：
--
发表时间：
2016
期刊：
USENIX Annual Technical Conference
影响因子：
--
作者：
Helgi Sigurbjarnarson;James Bornholt;Nicolas Christin;L. Cranor
通讯作者：
L. Cranor
带 CMC 的模型检查系统软件
DOI：
10.1145/1133373.1133418
发表时间：
2002
期刊：
2013 10th Working Conference on Mining Software Repositories (MSR)
影响因子：
--
作者：
M. Musuvathi;Andy Chou;D. Dill;D. Engler
通讯作者：
D. Engler
DOI：
--
发表时间：
2007
期刊：
--
影响因子：
--
作者：
Avi Kivity;Anthony Liguori
通讯作者：
Avi Kivity;Anthony Liguori
集群验证
DOI：
--
发表时间：
2008
期刊：
2008 23rd IEEE/ACM International Conference on Automated Software Engineering
影响因子：
--
作者：
G. Holzmann;Rajeev Joshi;Alex Groce
通讯作者：
Alex Groce
DOI：
10.1145/2815400.2815411
发表时间：
2015-10
期刊：
Proceedings of the 25th Symposium on Operating Systems Principles
影响因子：
--
作者：
T. Ridge;David Sheets;T. Tuerk;A. Giugliano;Anil Madhavapeddy;Peter Sewell
通讯作者：
T. Ridge;David Sheets;T. Tuerk;A. Giugliano;Anil Madhavapeddy;Peter Sewell