2018 | OriginalPaper | Chapter
Co-Design and Verification of an Available File System
Authors : Mahsa Najafzadeh, Marc Shapiro, Patrick Eugster
Published in: Verification, Model Checking, and Abstract Interpretation
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Distributed file systems play a vital role in large-scale enterprise services. However, the designer of a distributed file system faces a vexing choice between strong consistency and asynchronous replication. The former supports a standard sequential model by synchronising operations, but is slow and fragile. The latter is highly available and responsive, but exposes users to concurrency anomalies. In this paper, we describe a rigorous and general approach to navigating this trade-off by leveraging static verification tools that allow to verify different file system designs. We show that common file system operations can run concurrently without synchronisation, while still retaining a semantics reasonably similar to Posix hierarchical structure. The one exception is the $$\mathsf {move}$$ operation, for which we prove that, unless synchronised, it will have an anomalous behaviour.