Replication-aware Linearizability
Published in ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2019
Recommended citation: Chao Wang, Constantin Enea, Suha Mutluergil and Gustavo Petri. "Replication-aware Linearizability." In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019.
This paper proposes a new correctness criterion called RA-linearizability for distributed data types and shows that the well know CRDTs satisfy this new criterion in a natural way.
Abstract. Distributed systems often replicate data at multiple locations to achieve availability and performance 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 which 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.