Name
Abstract | ||
|---|---|---|
Distributed systems often replicate data at multiple locations to achieve availability despite network partitions. These systems accept updates at any replica and propagate them asynchronously to every other replica. Conflict-Free Replicated Data Types (CRDTs) provide a principled approach to the problem of ensuring that replicas are eventually consistent despite the asynchronous delivery of updates.
We address the problem of specifying and verifying CRDTs, introducing a new correctness criterion called Replication-Aware Linearizability. This criterion is inspired by linearizability, the de-facto correctness criterion for (shared-memory) concurrent data structures. We argue that this criterion is both simple to understand, and it fits most known implementations of CRDTs. We provide a proof methodology to show that a CRDT satisfies replication-aware linearizability that we apply on a wide range of implementations. Finally, we show that our criterion can be leveraged to reason modularly about the composition of CRDTs.
|
Year | DOI | Venue |
|---|---|---|
2019 | 10.1145/3314221.3314617 | Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation |
Keywords | DocType | Volume |
consistency, replicated data types, verification | Journal | abs/1903.06560 |
ISBN | Citations | PageRank |
978-1-4503-6712-7 | 0 | 0.34 |
References | Authors | |
0 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Constantin Enea | 1 | 249 | 26.95 |
| Suha Orhun Mutluergil | 2 | 0 | 0.34 |
| Gustavo Petri | 3 | 44 | 8.58 |
| Chao Wang | 4 | 895 | 190.04 |