Metis: File System Model Checking via Versatile Input and State Exploration

Explore a groundbreaking model-checking framework for file system testing in this conference talk from FAST '24. Dive into Metis, a versatile system designed for thorough and configurable input and state exploration. Learn about its nondeterministic loop and weighting scheme for executing system calls and arguments. Discover the innovative abstract state representation that supports efficient and effective state exploration. Understand how Metis compares file system behavior against a reference system, reports discrepancies, and aids in bug investigation and reproduction. Examine RefFS, a specially developed reference file system that accelerates model checking and enhances bug reproducibility. Analyze experimental results demonstrating Metis's flexible input generation and scalable state exploration across multiple nodes. Gain insights into the practical applications of Metis, including its role in identifying and fixing bugs in RefFS and other file systems, with real-world examples of confirmed and resolved issues in Linux.