Modern replicated data stores aim to provide high availability, by immediately responding to client requests, often by implementing objects that expose concurrency. Such objects, for example, multi-valued registers (MVRs), do not have sequential specifications. This talk explores 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 the following results:

• An eventually consistent data store implementing MVRs cannot satisfy a consistency model strictly stronger than observable causal consistency (OCC). OCC is a model somewhat stronger than causal consistency, which captures executions in which client observations can use causality to infer concurrency of operations. This result holds under certain assumptions about the data store.

• Under the same assumptions, an eventually consistent and causally consistent replicated data store must send messages of size linear in the size of the system: If S objects, each Ω(lg K)-bit in size, are supported by N replicas, then there is an execution in an Ω(min{N,S} K)-bit message is sent.

(Based on joint work with Hagit Attiya and Faith Ellen.)