Specification and complexity of replicated objects

Modern replicated data stores aim to provide high availability, by immediately responding to client requests, often by implementing objects that expose concurrency and do not have a sequential specification, like multi-valued registers (MVRs).

We explore a recent model for replicated data stores that can be used to precisely specify causal consistency for such objects, and liveness properties like eventual consistency, without revealing details of the underlying implementation. The model is used to prove what is the stronger consistency model that can be supported by an eventually consistent data store implementing MVRs, for a large class of protocols. For the same class, we prove that an eventually consistent and causally consistent replicated data store must send messages of unbounded size.

We further specify the list object, modeling the core functionality of replicated data stores for collaborative text editing and allowing users to concurrently edit a shared document, inserting and deleting elements (e.g., characters or lines). A major factor determining the efficiency and practical feasibility of a collaborative text editing protocol is the space overhead of its metadata. We prove that for a large class of protocols implementing a list, this space overhead is at least linear in the number of elements deleted from the list. A protocol in this class almost matches the lower bound.