Serializability for Eventual Consistency: Criterion, Analysis and Applications
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.
Thu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:20 - 16:00
|Mixed-size Concurrency: ARM, POWER, C/C++11, and SC|
Shaked Flur University of Cambridge, Susmit Sarkar University of St. Andrews, UK, Christopher Pulte University of Cambridge, Kyndylan Nienhuis University of Cambridge, Luc Maranget INRIA Rocquencourt, Kathryn E. Gray University of Cambridge, Ali Sezgin University of Cambridge, Mark Batty University of Kent, Peter Sewell University of Cambridge
|Dynamic Race Detection For C++11|
|Serializability for Eventual Consistency: Criterion, Analysis and Applications|
Lucas Brutschy ETH Zurich, Dimitar Dimitrov ETH Zurich, Switzerland, Peter Müller ETH Zurich, Martin Vechev ETH ZurichPre-print
|Thread Modularity at Many Levels: a Pearl in Compositional Verification|