The Taub Faculty of Computer Science Events and Talks

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.