Checking causal consistency of distributed databases

Computing (2021)Cite this article

Abstract

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.

Access options

Buy single article

Instant access to the full article PDF.

US$ 39.95

Tax calculation will be finalised during checkout.

Fig. 1
Fig. 2
Fig. 3

References

  1. 1.

    https://www.cockroachlabs.com, [Retrieved 15/11/2018]

  2. 2.

    http://galeracluster.com, [Retrieved 15/11/2018]

  3. 3.

    https://github.com/codership/galera/issues/336, [Retrieved 15/11/2018]

  4. 4.

    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

  5. 5.

    Abiteboul S, Hull R, Vianu V (eds) (1995) Foundations of databases: the logical level, 1st edn. Addison-Wesley Longman Publishing Co., Inc, Boston

    Google Scholar 

  6. 6.

    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

    MathSciNet  Article  MATH  Google Scholar 

  7. 7.

    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

  8. 8.

    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

  9. 9.

    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

  10. 10.

    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

  11. 11.

    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

  12. 12.

    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

  13. 13.

    Emmi M, Enea C (2018) Sound, complete, and tractable linearizability monitoring for concurrent collections. PACMPL 2:251–2527. https://doi.org/10.1145/3158113

    Article  Google Scholar 

  14. 14.

    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

  15. 15.

    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

    Article  Google Scholar 

  16. 16.

    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

    Article  Google Scholar 

  17. 17.

    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

    Article  MATH  Google Scholar 

  18. 18.

    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

    Article  MATH  Google Scholar 

  19. 19.

    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

  20. 20.

    Mahajan P, Alvisi L, Dahlin M (2011) Consistency, availability, convergence. Technical report

  21. 21.

    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

  22. 22.

    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

    Article  Google Scholar 

  23. 23.

    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

  24. 24.

    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

    Article  Google Scholar 

  25. 25.

    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

  26. 26.

    Warren DS (1999) Programming in tabled prolog. In: Symposium program, pp 62

  27. 27.

    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

    MathSciNet  Article  MATH  Google Scholar 

  28. 28.

    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

  29. 29.

    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

  30. 30.

    Zennou R, Biswas R, Bouajjani A, Enea C, Erradi M (2020) Checking causal consistency of distributed databases, https://arxiv.org/abs/2011.09753

  31. 31.

    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

Download references

Author information

Affiliations

  1. ENSIAS, Mohammed V University, Rabat, Morocco

    Rachid Zennou & Mohammed Erradi

  2. IRIF, CNRS, Université de Paris, 75013, Paris, France

    Rachid Zennou, Ranadeep Biswas, Ahmed Bouajjani & Constantin Enea

Authors
  1. Rachid Zennou
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ranadeep Biswas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ahmed Bouajjani
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Constantin Enea
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Mohammed Erradi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rachid Zennou.

Additional information

Publisher's Note

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 [29] and a more detailed version was published in arXiv [30]. 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.

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

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

Download citation

Keywords

  • Causal consistency
  • Causal memory
  • Causal convergence
  • Distributed databases
  • Formal verification
  • Testing

Mathematics Subject Classification

  • 68Q60