Skip to main content
USENIX
  • Conferences
  • Students
Sign in

connect with us


  •  Twitter
  •  Facebook
  •  LinkedIn
  •  Google+
  •  YouTube

twitter

Tweets by @usenix

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home » Using Model Checking to Find Serious File System Errors
Tweet

connect with us

Using Model Checking to Find Serious File System Errors

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 ``/''.

Junfeng Yang, Stanford University

Paul Twohey, Stanford University

Dawson Engler, Stanford University

Madanlal Musuvathi, Microsoft Research

BibTeX
@inproceedings {269480,
author = {Junfeng Yang and Paul Twohey and Dawson Engler and Madanlal Musuvathi},
title = {Using Model Checking to Find Serious File System Errors},
booktitle = {6th Symposium on Operating Systems Design \& Implementation (OSDI 04)},
year = {2004},
address = {San Francisco, CA},
url = {https://www.usenix.org/conference/osdi-04/using-model-checking-find-serious-file-system-errors},
publisher = {USENIX Association},
month = dec,
}
Download

Links

Paper: 
http://usenix.org/publications/library/proceedings/osdi04/tech/yang/yang.pdf
Paper (HTML): 
http://usenix.org/publications/library/proceedings/osdi04/tech/yang/yang_html/index.html
Award: 
Best Paper
  • Log in or    Register to post comments

© USENIX

  • Privacy Policy
  • Contact Us