A Modular Verification Methodology for Caching and Lock-Based Concurrency in File Systems

The Flashix project is a team effort to develop a functionally correct, crash-safe and concurrent file system for flash memory. The approach is based on encapsulated, modular components and their incremental refinement towards a realistic and executable implementation. Scala and C code is derived from the models. The file system provides strong guarantees in the presence of hardware failures and can tolerate crashes. It also performs internal operations in a concurrent thread of execution. This thesis emerged from this large-scale verification effort and reports on the verification methodology and its practical application to the file system. The first contribution is a modular approach for the specification and verification of crash-aware components. A component is crash-aware if it provides guarantees in the event of a power failure and subsequent recovery. A refinement theory is presented that facilitates increasing the atomicity of a component with respect to power failures incrementally. The semantics of the components capture the effect on a power failure of order-preserving write-back caches succinctly. This type of cache is common in journaling file systems. The semantics thereby ease the burden of specification significantly and the effect of a power failure propagates upwards a component hierarchy over every refinement step implicitly. The second contribution is an extension of this theory to concurrent, crash-aware components. This allows clients of a component to call interface operations concurrently as well as the component itself to perform internal operations in another thread of execution in the background. Lipton reduction is used to merge several steps into one block that is executed atomically. The approach ensures that not only atomicity with respect to concurrent threads is achieved, but also atomicity with respect to the crash behavior of the component. Opportunities for Lipton reductions are applied automatically based on annotations of ownership. The ownership discipline ensures that access to a data structure is possible only if the possession of sufficient permissions is proven. Permissions to a data structure are acquired by locking the mutex or reader-writer lock that synchronizes access to the data structure and relinquished by unlocking. The third contribution consists of the specification and verification of several components of the Flashix file system. The models include an erase block manager, a journal with transactions and garbage collection, a persistence layer with serialization and write-back caching for the journal and a component responsible for the atomicity of commits. The erase block manager hides the specific write characteristics of flash hardware and its error-prone nature from the rest of the file system. It performs wear-leveling concurrently in a background thread. For all components strong guarantees in the event of a power failure are proven. All proofs are mechanized in the tool KIV. Together the components comprise a coherent and working file system