Dates
Friday, January 07, 2022 - 03:00pm to Friday, January 07, 2022 - 04:30pm
Event Description

TITLE:

Model-Checking Support for File System Development

ABSTRACT:

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.

Contact events [at] cs.stonybrook.edu for zoom info. 

Event Title
Ph.D. Research Proficiency Presentation: Yifei Liu, File system dev with model checking