License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2019.30
URN: urn:nbn:de:0030-drops-109321
URL: http://drops.dagstuhl.de/opus/volltexte/2019/10932/
Go to the corresponding LIPIcs Volume Portal


Beillahi, Sidi Mohamed ; Bouajjani, Ahmed ; Enea, Constantin

Robustness Against Transactional Causal Consistency

pdf-format:
LIPIcs-CONCUR-2019-30.pdf (0.7 MB)


Abstract

Distributed storage systems and databases are widely used by various types of applications. Transactional access to these storage systems is an important abstraction allowing application programmers to consider blocks of actions (i.e., transactions) as executing atomically. For performance reasons, the consistency models implemented by modern databases are weaker than the standard serializability model, which corresponds to the atomicity abstraction of transactions executing over a sequentially consistent memory. Causal consistency for instance is one such model that is widely used in practice. In this paper, we investigate application-specific relationships between several variations of causal consistency and we address the issue of verifying automatically if a given transactional program is robust against causal consistency, i.e., all its behaviors when executed over an arbitrary causally consistent database are serializable. We show that programs without write-write races have the same set of behaviors under all these variations, and we show that checking robustness is polynomial time reducible to a state reachability problem in transactional programs over a sequentially consistent shared memory. A surprising corollary of the latter result is that causal consistency variations which admit incomparable sets of behaviors admit comparable sets of robust programs. This reduction also opens the door to leveraging existing methods and tools for the verification of concurrent programs (assuming sequential consistency) for reasoning about programs running over causally consistent databases. Furthermore, it allows to establish that the problem of checking robustness is decidable when the programs executed at different sites are finite-state.

BibTeX - Entry

@InProceedings{beillahi_et_al:LIPIcs:2019:10932,
  author =	{Sidi Mohamed Beillahi and Ahmed Bouajjani and Constantin Enea},
  title =	{{Robustness Against Transactional Causal Consistency}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Wan Fokkink and Rob van Glabbeek},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10932},
  URN =		{urn:nbn:de:0030-drops-109321},
  doi =		{10.4230/LIPIcs.CONCUR.2019.30},
  annote =	{Keywords: Distributed Databases, Causal Consistency, Model Checking}
}

Keywords: Distributed Databases, Causal Consistency, Model Checking
Seminar: 30th International Conference on Concurrency Theory (CONCUR 2019)
Issue Date: 2019
Date of publication: 26.08.2019


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