|
4th USENIX Conference on File and Storage Technologies—Abstract
Pp. 1–15 of the Proceedings
A Logic of File Systems
Muthian Sivathanu, Google Inc.; Andrea C. Arpaci-Dusseau, Remzi H. Arpaci-Dusseau, and Somesh Jha, University of Wisconsin, Madison
Abstract
Years of innovation in file systems have been highly successful
in improving their performance and functionality, but at the
cost of complicating their interaction with the disk. A variety of
techniques exist to ensure consistency and integrity of file system
data, but the precise set of correctness guarantees provided
by each technique is often unclear, making them hard to compare
and reason about. The absence of a formal framework has
hampered detailed verification of file system correctness.
We present a logical framework for modeling the interaction
of a file system with the storage system, and show how to apply
the logic to represent and prove correctness properties. We
demonstrate that the logic provides three main benefits. First, it
enables reasoning about existing file system mechanisms, allowing
developers to employ aggressive performance optimizations
without fear of compromising correctness. Second, the logic
simplifies the introduction and adoption of new file system functionality
by facilitating rigorous proof of their correctness. Finally,
the logic helps reason about smart storage systems that
track semantic information about the file system.
A key aspect of the logic is that it enables incremental modeling,
significantly reducing the barrier to entry in terms of its
actual use by file system designers. In general, we believe that
our framework transforms the hitherto esoteric and error-prone
"art" of file system design into a readily understandable and formally
verifiable process.
- View the full text of this paper in PDF.
Until December 2006, you will need your USENIX membership identification in order to access the full papers. The Proceedings are published as a collective work, © 2005 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.
