Metis: File System Model Checking via Versatile Input and State Exploration
summary
Metis is a model-checking framework that generates system-call sequences via a nondeterministic loop and weighting scheme, stores both concrete and compact abstract states, and differential-checks a tested file system against a reference. A new user-space reference FS, RefFS, provides a RefFS snapshot API for fast save/restore; RefFS explores states 3–28× faster than mature filesystems. Metis scales near-linearly across nodes, found and helped fix 11 RefFS bugs and reported 12 bugs in five other filesystems (five confirmed, one landed in Linux).
AI-written summary · about
chapters (10)
- 0:00Metis introduction
- 1:40Inputs and states in testing
- 3:49Metis design goals
- 7:25State exploration methods
- 10:16State save and restore
- 11:38Reference file system API
- 14:10Evaluation setup and results
- 17:47Performance and reliability
- 19:15Bug detection across FS
- 20:18Conclusion and open-source
related talks
12mUnderstanding and Finding Crash-Consistency Bugs in Parallel File Systems
16mA Model for Detecting Faults in Build Specifications
18mPreview: Verification (Correctness & Debugging)
18mAn Efficient Runtime Validation Framework based on the Theory of Refinement
20mScalable and Accurate Application-Level Crash-Consistency Testing(…)
23mMetamorphic Testing
55mMuch ado about testing
16mSEMSAN: a Configurable Sanitizer for Detecting System-Level Semantic Bugs