Skip to main content
SpringerLink
Log in

Checking Causal Consistency of Distributed Databases

  • Conference paper
  • First Online:
Networked Systems (NETYS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNCCN,volume 11704))

Included in the following conference series:

Abstract

Causal consistency is one of the strongest models that can be implemented to ensure availability and partition tolerance in distributed systems. In this paper, 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 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 is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. https://www.cockroachlabs.com. Accessed 15 Nov 2018

  2. http://galeracluster.com. Accessed 15 Nov 2018

  3. https://github.com/codership/galera/issues/336. Accessed 15 Nov 2018

  4. Abdulla, P.A., Haziza, F., Holík, L.: Parameterized verification through view abstraction. STTT 18(5), 495–516 (2016). https://doi.org/10.1007/s10009-015-0406-x

    Article  Google Scholar 

  5. Abiteboul, S., Hull, R., Vianu, V. (eds.): Foundations of Databases: The Logical Level, 1st edn. Addison-Wesley Longman Publishing Co., Inc., Boston (1995)

    Google Scholar 

  6. Ahamad, M., Neiger, G., Burns, J.E., Kohli, P., Hutto, P.W.: Causal memory: definitions, implementation, and programming. Distrib. Comput. 9(1), 37–49 (1995). https://doi.org/10.1007/BF01784241

    Article  MathSciNet  Google Scholar 

  7. Alur, R., McMillan, K.L., Peled, D.A.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160(1–2), 167–188 (2000). https://doi.org/10.1006/inco.1999.2847

    Article  MathSciNet  MATH  Google Scholar 

  8. Bailis, P., Ghodsi, A., Hellerstein, J.M., Stoica, I.: Bolt-on causal consistency. In: Proceedings of the 2013 ACM SIGMOD International Conference on Management of Data, SIGMOD 2013, pp. 761–772. ACM, New York (2013). https://doi.org/10.1145/2463676.2465279, http://doi.acm.org/10.1145/2463676.2465279

  9. Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On verifying causal consistency. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18–20 January 2017, pp. 626–638. ACM (2017). http://dl.acm.org/citation.cfm?id=3009888

  10. Bouajjani, A., Enea, C., Hamza, J.: Verifying eventual consistency of optimistic replication systems. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 285–296. ACM, New York (2014). https://doi.org/10.1145/2535838.2535877. http://doi.acm.org/10.1145/2535838.2535877

  11. Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: Zorn, B.G., Aiken, A. (eds.) Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, 5–10 June 2010, pp. 330–340. ACM (2010). https://doi.org/10.1145/1806596.1806634

  12. Du, J., Elnikety, S., Roy, A., Zwaenepoel, W.: Orbe: Scalable causal consistency using dependency matrices and physical clocks. In: Proceedings of the 4th Annual Symposium on Cloud Computing, SOCC 2013, pp. 11:1–11:14. ACM, New York (2013). https://doi.org/10.1145/2523616.2523628. http://doi.acm.org/10.1145/2523616.2523628

  13. Du, J., Iorgulescu, C., Roy, A., Zwaenepoel, W.: GentleRain: cheap and scalable causal consistency with physical clocks. In: Proceedings of the 5th ACM Symposium on Cloud Computing, SOCC 2014, November 2014. https://doi.org/10.1145/2670979.2670983

  14. Eiríksson, Á.T., McMillan, K.L.: Using formal verification/analysis methods on the critical path in system design: a case study. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 367–380. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60045-0_63

    Chapter  Google Scholar 

  15. Emmi, M., Enea, C.: Monitoring weak consistency. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 487–506. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_26

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  17. Emmi, M., Enea, C., Hamza, J.: 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, 15–17 June 2015, pp. 260–269. ACM (2015). https://doi.org/10.1145/2737924.2737983

  18. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992). https://doi.org/10.1145/146637.146681

    Article  MathSciNet  Google Scholar 

  19. Gilbert, S., Lynch, N.: Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News 33(2), 51–59 (2002). https://doi.org/10.1145/564585.564601

    Article  Google Scholar 

  20. Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990). https://doi.org/10.1145/78969.78972

    Article  Google Scholar 

  21. Jiménez, E., Fernández Anta, A., Cholvi, V.: A parametrized algorithm that implements sequential, causal, and cache memory consistencies. J. Syst. Softw. 81, 120–131 (2008). https://doi.org/10.1016/j.jss.2007.03.012

    Article  Google Scholar 

  22. Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690–691 (1979). https://doi.org/10.1109/TC.1979.1675439

    Article  MATH  Google Scholar 

  23. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978). https://doi.org/10.1145/359545.359563

    Article  MATH  Google Scholar 

  24. Lloyd, W., Freedman, M.J., Kaminsky, M., Andersen, D.G.: 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, pp. 401–416. ACM, New York (2011). https://doi.org/10.1145/2043556.2043593

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

    Google Scholar 

  26. Petersen, K., Spreitzer, M.J., Terry, D.B., Theimer, M.M., Demers, A.J.: Flexible update propagation for weakly consistent replication. SIGOPS Oper. Syst. Rev. 31(5), 288–301 (1997). https://doi.org/10.1145/269005.266711

    Article  Google Scholar 

  27. Preguiça, N., et al.: 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 2014, pp. 30–33. IEEE Computer Society, Washington, DC (2014). https://doi.org/10.1109/SRDSW.2014.33

  28. Qadeer, S.: Verifying sequential consistency on shared-memory multiprocessors by model checking. IEEE Trans. Parallel Distrib. Syst. 14(8), 730–741 (2003). https://doi.org/10.1109/TPDS.2003.1225053

    Article  Google Scholar 

  29. Vardi, M.Y.: The complexity of relational query languages (extended abstract). In: Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC 1982, pp. 137–146. ACM, New York (1982). https://doi.org/10.1145/800070.802186

  30. Wing, J.M., Gong, C.: Testing and verifying concurrent objects. J. Parallel Distrib. Comput. 17(1–2), 164–182 (1993). https://doi.org/10.1006/jpdc.1993.1015

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Rachid Zennou, Ranadeep Biswas, Ahmed Bouajjani & Constantin Enea

  2. ENSIAS, University Mohammed V, Rabat, Morocco

    Rachid Zennou & Mohammed Erradi

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 .

Editor information

Editors and Affiliations

  1. Uppsala University, Uppsala, Uppsala Län, Sweden

    Mohamed Faouzi Atig

  2. Augusta University, Augusta, GA, USA

    Alexander A. Schwarzmann

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Zennou, R., Biswas, R., Bouajjani, A., Enea, C., Erradi, M. (2019). Checking Causal Consistency of Distributed Databases. In: Atig, M., Schwarzmann, A. (eds) Networked Systems. NETYS 2019. Lecture Notes in Computer Science(), vol 11704. Springer, Cham. https://doi.org/10.1007/978-3-030-31277-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-31277-0_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-31276-3

  • Online ISBN: 978-3-030-31277-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation