License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2018.41
URN: urn:nbn:de:0030-drops-95799
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9579/
Go to the corresponding LIPIcs Volume Portal

Nagar, Kartik ; Jagannathan, Suresh

Automated Detection of Serializability Violations Under Weak Consistency

pdf-format:
LIPIcs-CONCUR-2018-41.pdf (0.6 MB)

Abstract

While a number of weak consistency mechanisms have been developed in recent years to improve performance and ensure availability in distributed, replicated systems, ensuring the correctness of transactional applications running on top of such systems remains a difficult and important problem. Serializability is a well-understood correctness criterion for transactional programs; understanding whether applications are serializable when executed in a weakly-consistent environment, however remains a challenging exercise. In this work, we combine a dependency graph-based characterization of serializability and leverage the framework of abstract executions to develop a fully-automated approach for statically finding bounded serializability violations under any weak consistency model. We reduce the problem of serializability to satisfiability of a formula in First-Order Logic (FOL), which allows us to harness the power of existing SMT solvers. We provide rules to automatically construct the FOL encoding from programs written in SQL (allowing loops and conditionals) and express consistency specifications as FOL formula. In addition to detecting bounded serializability violations, we also provide two orthogonal schemes to reason about unbounded executions by providing sufficient conditions (again, in the form of FOL formulae) whose satisfiability implies the absence of anomalies in any arbitrary execution. We have applied the proposed technique on TPC-C, a real-world database program with complex application logic, and were able to discover anomalies under Parallel Snapshot Isolation (PSI), and verify serializability for unbounded executions under Snapshot Isolation (SI), two consistency mechanisms substantially weaker than serializability.

BibTeX - Entry

@InProceedings{nagar_et_al:LIPIcs:2018:9579,
  author =	{Kartik Nagar and Suresh Jagannathan},
  title =	{{Automated Detection of Serializability Violations Under Weak Consistency}},
  booktitle =	{29th International Conference on Concurrency Theory  (CONCUR 2018)},
  pages =	{41:1--41:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Sven Schewe and Lijun Zhang},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9579},
  URN =		{urn:nbn:de:0030-drops-95799},
  doi =		{10.4230/LIPIcs.CONCUR.2018.41},
  annote =	{Keywords: Weak Consistency, Serializability, Database Applications}
}

Keywords: Weak Consistency, Serializability, Database Applications
Collection: 29th International Conference on Concurrency Theory (CONCUR 2018)
Issue Date: 2018
Date of publication: 31.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI