Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [45 references]  Display  Hide  Download
Contributor : Marc Shapiro Connect in order to contact the contributor
Submitted on : Tuesday, January 30, 2018 - 11:36:54 AM
Last modification on : Tuesday, March 23, 2021 - 9:28:03 AM
Long-term archiving on: : Friday, May 25, 2018 - 12:48:09 PM


Files produced by the author(s)



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⟩



Record views


Files downloads