Wed 20 Jun 2018 14:00 - 14:25 at Grand Ballroom AB - Concurrency and Termination Chair(s): Iulian Neamtiu

Many distributed databases provide only weak consistency guarantees to reduce synchronization overhead and remain available under network partitions. However, this leads to behaviors not possible under stronger guarantees. Such behaviors can easily defy programmer intuition and lead to errors that are notoriously hard to detect.

In this paper, we propose a static analysis for detecting non-serializable behaviors of applications running on top of causally-consistent databases. Our technique is based on a novel, local serializability criterion and combines a generalization of graph-based techniques from the database literature with another, complementary analysis technique that encodes our serializability criterion into first-order logic formulas to be checked by an SMT solver. This analysis is more expensive yet more precise and produces concrete counter-examples.

We implemented our methods and evaluated them on a number of applications from two different domains: cloud-backed mobile applications and clients of a distributed database. Our experiments demonstrate that our analysis is able to detect harmful serializability violations while producing only a small number of false alarms.

Wed 20 Jun
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

14:00 - 15:40: PLDI Research Papers - Concurrency and Termination at Grand Ballroom AB
Chair(s): Iulian NeamtiuNew Jersey Institute of Technology
pldi-2018-papers14:00 - 14:25
Lucas BrutschyETH Zurich, Dimitar DimitrovETH Zurich, Switzerland, Peter MüllerETH Zurich, Martin VechevETH Zürich
pldi-2018-papers14:25 - 14:50
Peizun LiuNortheastern University, USA, Thomas WahlNortheastern University
Media Attached
pldi-2018-papers14:50 - 15:15
Kostas FerlesUT Austin, Jacob Van GeffenUT Austin, Isil DilligUT Austin, Yannis SmaragdakisUniversity of Athens
Media Attached
pldi-2018-papers15:15 - 15:40
Yu-Fang Chen, Matthias HeizmannUniversity of Freiburg, Germany, Ondrej LengalBrno University of Technology , Yong LiInstitute of Software, Chinese Academy of Sciences, Ming-Hsien TsaiAcademia Sinica, Taiwan, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences
Media Attached