Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People

The Taub Faculty of Computer Science Events and Talks

Serializability Reasoning for Eventual Consistency
event speaker icon
Dimitar Dimitrov - GUEST LECTURE
event date icon
Tuesday, 27.03.2018, 14:30
event location icon
Room 337 Taub Bld.
High-availability requirements in modern software triggered the widespread adoption of eventually consistent data stores. Unfortunately, reasoning about the correctness of programs running under eventual consistency is a challenging task, largely due to the possibility of very weak system behaviors. In this talk, I will present new automated techniques that help developers precisely identify problematic weak behaviors. Our starting point will be to adopt conflict serializability as a correctness criterion. We then give a new generalized version that can reason about abstract data types under eventual consistency. This enables precise reasoning about data store clients that use commutative replicated data types. The generalization is founded in an abstract notion of operation dependency, which permits us to reason about dependencies between high-level operations. We show how to compute dependencies in practice by using two algebraic properties, namely, commutativity and absorption. This results in an effective dynamic serializability analysis based on cycle detection. In addition, we briefly discuss a static serializability analysis approach, but for a slightly stronger consistency property - causal consistency. Short Bio: ========== Dimitar Dimitrov is a PhD student at ETH Zurich working on analysis methods for concurrent and distributed programs. His research interests span program analysis, theory of concurrency, distributed computing, and logic.