Artifact Description:
This is the artifact for the FAST '24 paper "Metis: File System Model Checking via Versatile Input and State Exploration". Metis is a differential-testing-based model-checking framework designed for versatile, thorough, yet configurable file system testing in the form of input and state exploration. Metis can find file system bugs by comparing a file system under test to a reference file system, with the support of parallel/distributed state-space exploration and fast bug reproduction.

For more detailed documentation, please refer to the README of the Metis repository.

Paper:
Link to the USENIX FAST'24: https://www.usenix.org/conference/fast24/presentation/liu-yifei

Citation:
@INPROCEEDINGS{fast24metis,
TITLE = "{Metis}: File System Model Checking via Versatile Input and State Exploration",
AUTHOR = "Yifei Liu and Manish Adkar and Gerard Holzmann and Geoff Kuenning and Pei Liu and Scott Smolka and Wei Su and Erez Zadok",
NOTE = "To appear, won all 3 Artifact-Evaluation badges",
BOOKTITLE = "Proceedings of the 22nd USENIX Conference on File and Storage Technologies (FAST '24)",
ADDRESS = "Santa Clara, CA",
MONTH = "February",
YEAR = "2024",
PUBLISHER = "USENIX Association"
}

Estimated time to reproduce:
As a model-checking framework, it can run arbitrarily long time as long as the compute resources suffice. Also, the experimental duration highly depends on hardware specs and the number of Metis instances (i.e., Verification Tasks or VTs). However, for reproducing experiments in our paper, the estimated time duration is listed as follows.
Test Input Coverage: 5.3 hours.
Metis Performance and Scalability: 13 hours.
RefFS Performance and Reliability: 5 hours.
Bug Finding: each bug detection/reproduction takes a different time, but generally within 22 hours.

Reproducibility status:
This artifact was evaluated by USENIX FAST 2024 Artifact Evaluation Committee members and awarded all 3 Artifact-Evaluation badges: Artifacts Available, Artifacts Functional, and Results Reproduced.

DOI:
We also packaged this artifact via Zenodo with a permanent DOI. The link to the Zenodo archive is at https://zenodo.org/records/10537199 and the link to DOI is at https://doi.org/10.5281/zenodo.10537199

This artifact can be cited with DOI via the following BibTeX entry:
@misc{liu24metis-zenodo,
AUTHOR = "Yifei Liu and Manish Adkar and Gerard Holzmann and Geoff
Kuenning and Pei Liu and Scott Smolka and Wei Su and Erez Zadok",
title = "Artifact Package: the {Metis} File System Model Checking
Framework",
month = jan,
year = 2024,
publisher = "Zenodo",
version = "0.0.1",
doi = "10.5281/zenodo.10537199",
url = "https://doi.org/10.5281/zenodo.10537199"
}

Testbed:
The artifact requires x86 Ubuntu 20.04 or 22.04 with one of the following Linux kernel versions: 5.4.0, 5.15.0, 5.19.7, 6.0.6, 6.2.12, 6.3.0, or 6.6.1. It may work with other Linux distributions and kernels but we cannot guarantee that.

Support:
For any support, please email Yifei Liu (yifeliu@cs.stonybrook.edu) or create an issue at the GitHub repository.

Experiment Pattern:
This artifact generates one or multiple verifiers (or VTs) to run two file systems concurrently, and all the file system operations, file system states, and detected discrepancies are recorded in Metis logs. Any discrepancy is considered as a potential bug. Users can use these logs and saved file system images to confirm and reproduce file system bugs detected by Metis.