|
OSDI '04 — Abstract
Pp. 273–288 of the Proceedings
Awarded Best Paper!
Using Model Checking to Find Serious File System Errors
Junfeng Yang, Paul Twohey, and Dawson Engler, Stanford University; Madanlal Musuvathi, Microsoft Research
Abstract
This paper shows how to use model checking to find serious
errors in file systems. Model checking is a formal verification
technique tuned for finding corner-case errors by comprehensively
exploring the state spaces defined by a system.
File systems
have two dynamics that make them attractive for such an approach.
First, their errors are some of the most serious, since they can
destroy
persistent data and lead to unrecoverable
corruption. Second, traditional testing needs an impractical,
exponential number of test cases to check that the system will recover
if it crashes at any point during execution. Model checking employs a
variety of state-reducing techniques that allow it to explore such vast
state spaces efficiently.
We built a system, FiSC, for model checking file systems.
We applied it to three widely-used,
heavily-tested file systems:
ext3 [13],
JFS [21],
and
ReiserFS [27].
We found serious bugs in all of them, 32 in
total. Most have led to patches within a day of
diagnosis. For each file system, FiSC found demonstrable
events leading to the unrecoverable destruction of metadata and entire
directories, including the file system root directory ``/''.
- View the full text of this paper in HTML and
PDF.
The Proceedings are published as a collective work, © 2004 by the USENIX Association. All Rights Reserved. Rights to individual papers remain with the author or the author's employer. Permission is granted for the noncommercial reproduction of the complete work for educational or research purposes. USENIX acknowledges all trademarks within this paper.
- If you need the latest Adobe Acrobat Reader, you can download it from Adobe's site.
|
Need help? Use our Contacts page.
