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

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:40
Concurrency and TerminationPLDI Research Papers at Grand Ballroom AB
Chair(s): Iulian Neamtiu New Jersey Institute of Technology
14:00
25m
Talk
Static Serializability Analysis for Causal Consistency
PLDI Research Papers
Lucas Brutschy ETH Zurich, Dimitar Dimitrov ETH Zurich, Switzerland, Peter Müller ETH Zurich, Martin Vechev ETH Zürich
14:25
25m
Talk
CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs
PLDI Research Papers
Peizun Liu Northeastern University, USA, Thomas Wahl Northeastern University
Media Attached
14:50
25m
Talk
Symbolic Reasoning for Automatic Signal Placement
PLDI Research Papers
Kostas Ferles UT Austin, Jacob Van Geffen UT Austin, Isil Dillig UT Austin, Yannis Smaragdakis University of Athens
Media Attached
15:15
25m
Talk
Advanced Automata-Based Algorithms for Program Termination Checking
PLDI Research Papers
Yu-Fang Chen , Matthias Heizmann University of Freiburg, Germany, Ondřej Lengál Brno University of Technology , Yong Li Institute of Software, Chinese Academy of Sciences, Ming-Hsien Tsai Academia Sinica, Taiwan, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences
Media Attached