Co-Design and Verification of an Available File System

Abstract : 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 replica-tion. 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 move operation, for which we prove that, unless synchronised, it will have an anomalous behaviour.
Document type :
Conference papers
Complete list of metadatas

Cited literature [45 references]  Display  Hide  Download

https://hal.inria.fr/hal-01696263
Contributor : Marc Shapiro <>
Submitted on : Tuesday, January 30, 2018 - 11:36:54 AM
Last modification on : Friday, July 5, 2019 - 3:26:03 PM
Long-term archiving on : Friday, May 25, 2018 - 12:48:09 PM

File

VMCAI-2018-filesys.pdf
Files produced by the author(s)

Identifiers

Citation

Mahsa Najafzadeh, Marc Shapiro, Patrick Eugster. Co-Design and Verification of an Available File System. VMCAI 2018 - International Conference on Verification, Model Checking, and Abstract Interpretation, Jan 2018, Los Angeles, CA, United States. pp.358-381, ⟨10.1007/978-3-319-73721-8_17⟩. ⟨hal-01696263⟩

Share

Metrics

Record views

268

Files downloads

130