POPL 2017
Sun 15 - Sat 21 January 2017
Thu 19 Jan 2017 15:10 - 15:35 at Amphitheater 44 - Concurrency 2 Chair(s): Nobuko Yoshida

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 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00: Concurrency 2POPL at Amphitheater 44
Chair(s): Nobuko YoshidaImperial College London, UK
14:20 - 14:45
Shaked FlurUniversity of Cambridge, Susmit SarkarUniversity of St. Andrews, UK, Christopher PulteUniversity of Cambridge, Kyndylan NienhuisUniversity of Cambridge, Luc MarangetINRIA Rocquencourt, Kathryn E. GrayUniversity of Cambridge, Ali SezginUniversity of Cambridge, Mark BattyUniversity of Kent, Peter SewellUniversity of Cambridge
14:45 - 15:10
Christopher LidburyImperial College London, Alastair DonaldsonImperial College London
15:10 - 15:35
Lucas BrutschyETH Zurich, Dimitar DimitrovETH Zurich, Switzerland, Peter MüllerETH Zurich, Martin VechevETH Zurich
15:35 - 16:00
Jochen HoenickeUniversität Freiburg, Rupak MajumdarMPI-SWS, Andreas PodelskiUniversity of Freiburg, Germany