Experiences with Formal Specification of Fault-Tolerant File Systems

Roxana Geambasu, John MacCormick, Andrew Birrell

Proceedings of the 38th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN-DCCS), April, 2008

Abstract

Fault-tolerant, replicated file systems are a crucial component of today’s data centers. Despite their huge complexity, these systems are typically specified only in brief prose, which makes them difficult to reason about or verify. This paper describes the authors’ experience using formal methods to improve our understanding of and confidence in the behavior of replicated file systems. We wrote formal specifications for three real-world fault-tolerant file systems and used them to: (1) expose design similarities and differences; (2) clarify and mechanically verify consistency properties; and (3) evaluate design alternatives. Our experience showed that formal specifications for these systems were easy to produce, useful for a deep understanding of system functions, and valuable for system comparison.

PDF

dccs08geambasu

Columbia University Department of Computer Science