Developing and reasoning about systems using eventually consistent data stores is a difficult challenge due to the presence of behaviors that do not occur under sequential consistency. A fundamental problem in this setting is to identify a correctness criterion that precisely captures intended application behaviors yet is generic in nature.

In this paper, we present such a criterion. More formally, we generalize conflict serializability to the setting of eventual consistency. Our generalization is based on a novel dependency model that incorporates two powerful algebraic properties: commutativity and absorption. This enables precise reasoning about programs that employ high-level replicated data types, common in modern systems. To apply our criterion in practice, we also developed a dynamic analysis algorithm and a tool which checks whether a given program execution is serializable.

We performed a thorough experimental evaluation on two real world use cases: debugging cloud-backed mobile applications and implementing clients of a popular eventually consistent key-value store. Our experimental results indicate that our criterion matches programmers’ intuitive notion of correctness, is more effective at finding bugs than prior approaches, and can be used during the development of practical, eventually consistent applications.