TY - GEN
T1 - Model-checking support for file system development
AU - Su, Wei
AU - Liu, Yifei
AU - Ganesan, Gomathi
AU - Holzmann, Gerard
AU - Smolka, Scott
AU - Zadok, Erez
AU - Kuenning, Geoff
N1 - Publisher Copyright:
© 2021 Copyright held by the owner/author(s).
PY - 2021/7/20
Y1 - 2021/7/20
N2 - 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.
AB - 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.
KW - File systems
KW - Model checking
KW - Verification
UR - https://www.scopus.com/pages/publications/85112055541
U2 - 10.1145/3465332.3470878
DO - 10.1145/3465332.3470878
M3 - Conference contribution
AN - SCOPUS:85112055541
T3 - HotStorage 2021 - Proceedings of the 13th ACM Workshop on Hot Topics in Storage and File Systems
SP - 103
EP - 110
BT - HotStorage 2021 - Proceedings of the 13th ACM Workshop on Hot Topics in Storage and File Systems
PB - Association for Computing Machinery, Inc
T2 - 13th ACM Workshop on Hot Topics In Storage and File Systems, HotStorage 2021
Y2 - 27 July 2021 through 28 July 2021
ER -