The CAP Theorem shows that (strong) consistency, availability, and partition tolerance are impossible to be ensured together. Causal consistency is one of the weak consistency models that can be implemented to ensure availability and partition tolerance in distributed systems. In this work, we propose a tool to check automatically the conformance of distributed/concurrent systems executions to causal consistency models. Our approach consists in reducing the problem of checking if an execution is causally consistent to solving datalog queries. The reduction is based on complete characterizations of the executions violating causal consistency in terms of the existence of cycles in suitably defined relations between the operations occurring in these executions. We have implemented the reduction in a testing tool for distributed databases, and carried out several experiments on real case studies, showing the efficiency of the suggested approach.
This is a preview of subscription content, access via your institution.
Buy single article
Instant access to the full article PDF.
Tax calculation will be finalised during checkout.
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
Tax calculation will be finalised during checkout.
https://www.cockroachlabs.com, [Retrieved 15/11/2018]
http://galeracluster.com, [Retrieved 15/11/2018]
https://github.com/codership/galera/issues/336, [Retrieved 15/11/2018]
Abdulla PA, Atig MF, Jonsson B, Lång M, Ngo TP, Sagonas K (2019) Optimal stateless model checking for reads-from equivalence under sequential consistency. Proc. ACM Program. Lang. 3(OOPSLA) https://doi.org/10.1145/3360576
Abiteboul S, Hull R, Vianu V (eds) (1995) Foundations of databases: the logical level, 1st edn. Addison-Wesley Longman Publishing Co., Inc, Boston
Ahamad M, Neiger G, Burns JE, Kohli P, Hutto PW (1995) Causal memory: Definitions, implementation, and programming. Distrib Comput 9(1):37–49. https://doi.org/10.1007/BF01784241
Bailis P, Ghodsi A, Hellerstein JM, Stoica I (2013) Bolt-on causal consistency. In: Proceedings of the 2013 ACM SIGMOD international conference on management of data. SIGMOD ’13, ACM, New York, NY, USA, pp 761–772, http://doi.acm.org/10.1145/2463676.2465279
Bouajjani A, Enea C, Guerraoui R, Hamza J (2017) On verifying causal consistency. In: Castagna G, Gordon AD (eds) Proceedings of the 44th ACM SIGPLAN symposium on principles of programming languages, POPL 2017, Paris, France, January 18–20. ACM, pp 626–638, http://dl.acm.org/citation.cfm?id=3009888
Bouajjani A, Enea C, Hamza J (2014) Verifying eventual consistency of optimistic replication systems. In: Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages. POPL ’14, ACM, New York, NY, USA, pp 285–296, http://doi.acm.org/10.1145/2535838.2535877
Burckhardt S, Dern C, Musuvathi M, Tan R (2010) Line-up: a complete and automatic linearizability checker. In: Zorn BG, Aiken A (eds) Proceedings of the 2010 ACM SIGPLAN conference on programming language design and implementation, PLDI 2010, Toronto, Ontario, Canada, June 5–10. ACM, pp 330–340, https://doi.org/10.1145/1806596.1806634
Du J, Elnikety S, Roy A, Zwaenepoel W (2013) Orbe: scalable causal consistency using dependency matrices and physical clocks. In: Proceedings of the 4th annual symposium on cloud computing. SOCC ’13, ACM, New York, NY, USA, pp 11:1–11:14, http://doi.acm.org/10.1145/2523616.2523628
Emmi M, Enea C (2018) Monitoring weak consistency. In: Chockler H, Weissenbacher G (eds) Computer aided verification - 30th international conference, CAV 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018, Proceedings, Part I. Lecture notes in computer science, vol 10981. Springer, pp 487–506, https://doi.org/10.1007/978-3-319-96145-3_26
Emmi M, Enea C (2018) Sound, complete, and tractable linearizability monitoring for concurrent collections. PACMPL 2:251–2527. https://doi.org/10.1145/3158113
Emmi M, Enea C, Hamza J (2015) Monitoring refinement via symbolic reasoning. In: Grove D, Blackburn S (eds) Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation, Portland, OR, USA, June 15-17, 2015. ACM, pp 260–269, https://doi.org/10.1145/2737924.2737983
Gilbert S, Lynch N (2002) Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News 33(2):51–59. https://doi.org/10.1145/564585.564601
Herlihy MP, Wing JM (1990) Linearizability: a correctness condition for concurrent objects. ACM Trans Program Lang Syst 12(3):463–492. https://doi.org/10.1145/78969.78972
Lamport L (1979) How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans Comput 28(9):690–691. https://doi.org/10.1109/TC.1979.1675439
Lamport L (1978) Time, clocks, and the ordering of events in a distributed system. Commun ACM 21(7):558–565. https://doi.org/10.1145/359545.359563
Lloyd W, Freedman MJ, Kaminsky M, Andersen DG (2011) Don’t settle for eventual: scalable causal consistency for wide-area storage with cops. In: proceedings of the twenty-third ACM symposium on operating systems principles. SOSP ’11, ACM, New York, NY, USA, pp 401–416, http://doi.acm.org/10.1145/2043556.2043593
Mahajan P, Alvisi L, Dahlin M (2011) Consistency, availability, convergence. Technical report
Perrin M, Mostefaoui A, Jard C (2016) Causal consistency: beyond memory. In: Proceedings of the 21st ACM SIGPLAN symposium on principles and practice of parallel programming. PPoPP ’16, ACM, New York, NY, USA, pp 26:1–26:12
Petersen K, Spreitzer MJ, Terry DB, Theimer MM, Demers AJ (1997) Flexible update propagation for weakly consistent replication. SIGOPS Oper Syst Rev 31(5):288–301. https://doi.org/10.1145/269005.266711
Preguiça N, Zawirski M, Bieniusa A, Duarte S, Balegas V, Baquero C, Shapiro M (2014) Swiftcloud: fault-tolerant geo-replication integrated all the way to the client machine. In: Proceedings of the 2014 IEEE 33rd international symposium on reliable distributed systems workshops. SRDSW ’14, IEEE Computer Society, Washington, DC, USA, pp 30–33, https://doi.org/10.1109/SRDSW.2014.33
Qadeer S (2003) Verifying sequential consistency on shared-memory multiprocessors by model checking. IEEE Trans Parallel Distrib Syst 14(8):730–741. https://doi.org/10.1109/TPDS.2003.1225053
Vardi M.Y (1982) The complexity of relational query languages (extended abstract). In: Proceedings of the fourteenth annual ACM symposium on theory of computing. STOC ’82, ACM, New York, NY, USA, pp 137–146, http://doi.acm.org/10.1145/800070.802186
Warren DS (1999) Programming in tabled prolog. In: Symposium program, pp 62
Wing JM, Gong C (1993) Testing and verifying concurrent objects. J Parallel Distrib Comput 17(1–2):164–182. https://doi.org/10.1006/jpdc.1993.1015
Zennou R, Atig MF, Biswas R, Bouajjani A, Enea C, Erradi M (2020) Boosting sequential consistency checking using saturation. In: Hung DV, Sokolsky O (eds) Automated technology for verification and analysis. Springer, Cham, pp 360–376. https://doi.org/10.1007/978-3-030-59152-6_20
Zennou R, Biswas R, Bouajjani A, Enea C, Erradi M (2019) Checking causal consistency of distributed databases. In: Atig MF, Schwarzmann AA (eds) Networked systems. Springer International Publishing, Cham, pp 35–51 https://doi.org/10.1007/978-3-030-31277-0_3
Zennou R, Biswas R, Bouajjani A, Enea C, Erradi M (2020) Checking causal consistency of distributed databases, https://arxiv.org/abs/2011.09753
Zennou R, Bouajjani A, Enea C, Erradi M (2019) Gradual consistency checking. In: Dillig I, Tasiran S, (eds) Computer Aided Verification. Springer, Cham, pp 267–285, https://doi.org/10.1007/978-3-030-25543-5_16
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
This is an extended version of a paper published in NETYS’2019 proceeding  and a more detailed version was published in arXiv . This work is supported in part by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant Agreement No. 678177). This work is also supported by Centre National pour la Recherche Scientifique et Technique (CNRST) Morocco.
About this article
Cite this article
Zennou, R., Biswas, R., Bouajjani, A. et al. Checking causal consistency of distributed databases. Computing (2021). https://doi.org/10.1007/s00607-021-00911-3
- Causal consistency
- Causal memory
- Causal convergence
- Distributed databases
- Formal verification
Mathematics Subject Classification