A Logic of File Systems
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, enabling 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 {\em 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.
Download:[PS,PDF]
Somesh Jha
Last modified: Tue Sep 19 14:13:07 CDT 2006