A Framework for Transactional Consistency Models with Atomic Visibility

Authors Andrea Cerone, Giovanni Bernardi, Alexey Gotsman

Thumbnail PDF


  • Filesize: 0.74 MB
  • 14 pages

Document Identifiers

Author Details

Andrea Cerone
Giovanni Bernardi
Alexey Gotsman

Cite AsGet BibTex

Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. A Framework for Transactional Consistency Models with Atomic Visibility. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 58-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Modern distributed systems often rely on databases that achieve scalability by providing only weak guarantees about the consistency of distributed transaction processing. The semantics of programs interacting with such a database depends on its consistency model, defining these guarantees. Unfortunately, consistency models are usually stated informally or using disparate formalisms, often tied to the database internals. To deal with this problem, we propose a framework for specifying a variety of consistency models for transactions uniformly and declaratively. Our specifications are given in the style of weak memory models, using structures of events and relations on them. The specifications are particularly concise because they exploit the property of atomic visibility guaranteed by many consistency models: either all or none of the updates by a transaction can be visible to another one. This allows the specifications to abstract from individual events inside transactions. We illustrate the use of our framework by specifying several existing consistency models. To validate our specifications, we prove that they are equivalent to alternative operational ones, given as algorithms closer to actual implementations. Our work provides a rigorous foundation for developing the metatheory of the novel form of concurrency arising in weakly consistent large-scale databases.
  • Replication
  • Consistency models
  • Transactions


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Daniel Abadi. Consistency tradeoffs in modern distributed database system design: CAP is only part of the story. IEEE Computer, 45(2), 2012. Google Scholar
  2. Atul Adya. Weak consistency: A generalized theory and optimistic implementations for distributed transactions. PhD thesis, MIT, 1999. Google Scholar
  3. Jade Alglave. A formal hierarchy of weak memory models. FMSD, 41(2), 2012. Google Scholar
  4. Peter Bailis, Aaron Davidson, Alan Fekete, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. Highly Available Transactions: virtues and limitations. In VLDB, 2014. Google Scholar
  5. Peter Bailis, Alan Fekete, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. The potential dangers of causal consistency and an explicit solution. In SOCC, 2012. Google Scholar
  6. Peter Bailis, Alan Fekete, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. Scalable atomic visibility with RAMP transactions. In SIGMOD, 2014. Google Scholar
  7. Mark Batty, Mike Dodds, and Alexey Gotsman. Library abstraction for C/C++ concurrency. In POPL, 2013. Google Scholar
  8. Hal Berenson, Phil Bernstein, Jim Gray, Jim Melton, Elizabeth O'Neil, and Patrick O'Neil. A critique of ANSI SQL isolation levels. In SIGMOD, 1995. Google Scholar
  9. Kenneth P. Birman and Thomas A. Joseph. Reliable communication in the presence of failures. ACM Trans. Comput. Syst., 5(1), 1987. Google Scholar
  10. Roberto Bruni, Hernán C. Melgratti, and Ugo Montanari. cJoin: Join with communicating transactions. Mathematical Structures in Computer Science, 25(3), 2015. Google Scholar
  11. Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. Replicated data types: specification, verification, optimality. In POPL, 2014. Google Scholar
  12. Sebastian Burckhardt, Daan Leijen, Manuel Fähndrich, and Mooly Sagiv. Eventually consistent transactions. In ESOP, 2012. Google Scholar
  13. Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel Fähndrich. Global sequence protocol: A robust abstraction for replicated shared state. In ECOOP, 2015. Google Scholar
  14. Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. A framework for transactional consistency models with atomic visibility (extended version). Available from URL: http://software.imdea.org/~gotsman/.
  15. Vincent Danos and Jean Krivine. Transactions in RCCS. In CONCUR, 2005. Google Scholar
  16. Rocco De Nicola and Matthew Hennessy. Testing equivalence for processes. In ICALP, 1983. Google Scholar
  17. Vasileios Koutavas, Carlo Spaccasassi, and Matthew Hennessy. Bisimulations for communicating transactions (extended abstract). In FOSSACS, 2014. Google Scholar
  18. Cheng Li, Daniel Porto, Allen Clement, Rodrigo Rodrigues, Nuno Preguiça, and Johannes Gehrke. Making geo-replicated systems fast if possible, consistent when necessary. In OSDI, 2012. Google Scholar
  19. Wyatt Lloyd, Michael J. Freedman, Michael Kaminsky, and David G. Andersen. Don't settle for eventual: scalable causal consistency for wide-area storage with COPS. In SOSP, 2011. Google Scholar
  20. Christos H. Papadimitriou. The serializability of concurrent database updates. J. ACM, 26(4), 1979. Google Scholar
  21. M. Saeida Ardekani, P. Sutra, and M. Shapiro. Non-monotonic snapshot isolation: Scalable and strong consistency for geo-replicated transactional systems. In SRDS, 2013. Google Scholar
  22. M. Saeida Ardekani, P. Sutra, M. Shapiro, and N. Preguiça. On the scalability of snapshot isolation. In Euro-Par, 2013. Google Scholar
  23. Marc Shapiro, Nuno M. Preguiça, Carlos Baquero, and Marek Zawirski. Conflict-free replicated data types. In SSS, 2011. Google Scholar
  24. Y. Sovran, R. Power, M. K. Aguilera, and J. Li. Transactional storage for geo-replicated systems. In SOSP, 2011. Google Scholar
  25. Douglas B. Terry, Alan J. Demers, Karin Petersen, Mike Spreitzer, Marvin Theimer, and Brent W. Welch. Session guarantees for weakly consistent replicated data. In PDIS, 1994. Google Scholar
  26. Glynn Winskel. Event structure semantics for CCS and related languages. In ICALP, 1982. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail