Abstract | ||
---|---|---|
Recent storage systems trade strong consistency for performance, availability, and scalability. However, this makes it hard to understand the semantics that the storage system provides, and also makes the design and implementation of the storage system itself more error-prone. This paper proposes a comprehensive solution to these problems. In particular, we propose a specification language named ConSpec, which enables the formalization of different consistency semantics that a storage system may provide, using a uniform syntax that is independent of the design and implementation of the target storage system. We use ConSpec to revisit several existing models in light of a common way to define and compare them. Furthermore, we generalize the CAP theorem, whose original formulation only considered linearizability, to precisely define the class of consistency definitions that can and cannot be implemented in a highly-available, partition-tolerant way. Finally, we present the design and implementation of a new consistency checker that takes a trace from a storage system (e.g., the output of a test suite) and validates whether it meets any consistency semantics defined using ConSpec. The evaluation of our consistency checker shows that it is able to verify the correctness of long traces in a reasonable time. |
Year | DOI | Venue |
---|---|---|
2019 | 10.1109/SRDS47363.2019.00027 | 2019 38th Symposium on Reliable Distributed Systems (SRDS) |
Keywords | DocType | ISSN |
Consistency,specification,verification,storage system,distributed system | Conference | 1060-9857 |
ISBN | Citations | PageRank |
978-1-7281-4223-4 | 0 | 0.34 |
References | Authors | |
23 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Subhajit Sidhanta | 1 | 17 | 3.84 |
Ricardo J. Dias | 2 | 35 | 6.27 |
Rodrigo Rodrigues | 3 | 43 | 4.86 |