Algebraic Laws for Weak Consistency

Authors Andrea Cerone, Alexey Gotsman, Hongseok Yang

Thumbnail PDF


  • Filesize: 0.64 MB
  • 18 pages

Document Identifiers

Author Details

Andrea Cerone
Alexey Gotsman
Hongseok Yang

Cite AsGet BibTex

Andrea Cerone, Alexey Gotsman, and Hongseok Yang. Algebraic Laws for Weak Consistency. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Modern distributed systems often rely on so called weakly consistent databases, which achieve scalability by weakening consistency guarantees of distributed transaction processing. The semantics of such databases have been formalised in two different styles, one based on abstract executions and the other based on dependency graphs. The choice between these styles has been made according to intended applications. The former has been used for specifying and verifying the implementation of the databases, while the latter for proving properties of client programs of the databases. In this paper, we present a set of novel algebraic laws (inequalities) that connect these two styles of specifications. The laws relate binary relations used in a specification based on abstract executions to those used in a specification based on dependency graphs. We then show that this algebraic connection gives rise to so called robustness criteria: conditions which ensure that a client program of a weakly consistent database does not exhibit anomalous behaviours due to weak consistency. These criteria make it easy to reason about these client programs, and may become a basis for dynamic or static program analyses. For a certain class of consistency models specifications, we prove a full abstraction result that connects the two styles of specifications.
  • Weak Consistency Models
  • Distributed Databases
  • Dependency Graphs


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


  1. Atul Adya. Weak consistency: A generalized theory and optimistic implementations for distributed transactions. PhD thesis, MIT, 1999. Google Scholar
  2. Jade Alglave, Daniel Kroening, Vincent Nimal, and Daniel Poetzl. Don't sit on the fence: A static analysis approach to automatic fence insertion. ACM Transactions on Programming Languages Systems, 39(2):6:1-6:38, 2017. Google Scholar
  3. Jade Alglave and Luc Maranget. Stability in weak memory models. In International Confence on Computer Aided Verification (CAV), pages 50-66, 2011. Google Scholar
  4. Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Transactions on Programming Languages Systems, 36(2):7:1-7:74, 2014. Google Scholar
  5. Peter Bailis, Alan Fekete, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. Scalable atomic visibility with RAMP transactions. In 2014 ACM SIGMOD International Conference on Management of Data (SIGMOD), pages 27-38, 2014. Google Scholar
  6. Hal Berenson, Phil Bernstein, Jim Gray, Jim Melton, Elizabeth O'Neil, and Patrick O'Neil. A critique of ANSI SQL isolation levels. In 1995 ACM SIGMOD international conference on Management of data (SIGMOD), pages 1-10, 1995. Google Scholar
  7. Giovanni Bernardi and Alexey Gotsman. Robustness against consistency models with atomic visibility. In 27th International Conference on Concurrency Theory (CONCUR), pages 7:1-7:15, 2016. URL:
  8. Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. Checking and enforcing robustness against TSO. In 23rd European Symposium on Programming (ESOP), pages 533-553, 2013. Google Scholar
  9. Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza. On verifying causal consistency. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 626-638, 2017. Google Scholar
  10. Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev. Serializability for eventual consistency: Criterion, analysis and applications. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, January 2017. Google Scholar
  11. Sebastian Burckhardt. Principles of eventual consistency. Foundations and Trends in Programming Languages, 1(1-2):1-150, 2014. URL:
  12. Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen, and Mooly Sagiv. Eventually consistent transactions. In 22nd European Symposium on Programming (ESOP), page 67–86, 2012. URL:
  13. Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. Replicated data types: specification, verification, optimality. In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 271-284, 2014. Google Scholar
  14. Simon Castellan. Weak memory models using event structures. In Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), 2016. Google Scholar
  15. Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. A framework for transactional consistency models with atomic visibility. In 26th International Conference on Concurrency Theory (CONCUR), pages 58-71. Dagstuhl, 2015. Google Scholar
  16. Andrea Cerone and Alexey Gotsman. Analysing snapshot isolation. In 2016 ACM Symposium on Principles of Distributed Computing (PODC), pages 55-64, 2016. Google Scholar
  17. Andrea Cerone, Alexey Gotsman, and Hongseok Yang. Algebraic laws for weak consistency (extended version). URL:
  18. Andrea Cerone, Alexey Gotsman, and Hongseok Yang. Transaction chopping for parallel snapshot isolation. In 29th International Symposium on Distributed Computing (DISC), pages 388-404, 2015. Google Scholar
  19. Alan Fekete, Dimitrios Liarokapis, Elizabeth O'Neil, Patrick O'Neil, and Dennis Shasha. Making snapshot isolation serializable. ACM Transactions on Database Systems, 30(2):492-528, 2005. Google Scholar
  20. Alexey Gotsman and Hongseok Yang. Composite replicated data types. In Jan Vitek, editor, 24th European Symposium on Programming (ESOP), pages 585-609, 2015. Google Scholar
  21. Alan Jeffrey and James Riely. On thin air reads towards an event structures model of relaxed memory. In 31st ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 759-767, 2016. Google Scholar
  22. Dexter Kozen and Frederick Smith. Kleene algebra with tests: Completeness and decidability. In 10th International Workshop on Computer Science Logic (CSL), pages 244-259. Springer-Verlag, 1996. Google Scholar
  23. Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Preguiça, and Rodrigo Rodrigues. Making geo-replicated systems fast as possible, consistent when necessary. In 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 265-278, 2012. Google Scholar
  24. 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 23rd ACM Symposium on Operating Systems Principles (SOSP), pages 401-416, 2011. Google Scholar
  25. Microsoft SQL server documentation, Set Transaction Isolation Level. URL:
  26. M. Saeida Ardekani, P. Sutra, and M. Shapiro. Non-monotonic snapshot isolation: Scalable and strong consistency for geo-replicated transactional systems. In 32nd International Symposium on Reliable Distributed Systems (SRDS), pages 163-172, 2013. Google Scholar
  27. D. Shasha, F. Llirbat, E. Simon, and P. Valduriez. Transaction chopping: Algorithms and performance studies. ACM Trans. Database Syst., 20(3):325-363, 1995. Google Scholar
  28. Y. Sovran, R. Power, M. K. Aguilera, and J. Li. Transactional storage for geo-replicated systems. In 23rd ACM Symposium on Operating Systems Principles (SOSP), pages 385-400, 2011. Google Scholar
  29. Douglas B Terry, Alan J Demers, Karin Petersen, Mike J Spreitzer, Marvin M Theimer, and Brent B Welch. Session guarantees for weakly consistent replicated data. In 3rd International Conference on Parallel and Distributed Information Systems (PDIS), pages 140-149. IEEE, 1994. Google Scholar
  30. Paolo Viotti and Marko Vukolić. Consistency in non-transactional distributed storage systems. ACM Computing Surveys, 49(1):19:1-19:34, 2016. URL:
  31. Kamal Zellag and Bettina Kemme. Consistency anomalies in multi-tier architectures: Automatic detection and prevention. The VLDB Journal, 23(1):147-172, 2014. Google Scholar