Checking Causal Consistency of Distributed Databases

  • Rachid ZennouEmail author
  • Ranadeep Biswas
  • Ahmed Bouajjani
  • Constantin Enea
  • Mohammed Erradi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11704)


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.


  1. 1. Accessed 15 Nov 2018
  2. 2. Accessed 15 Nov 2018
  3. 3.
  4. 4.
    Abdulla, P.A., Haziza, F., Holík, L.: Parameterized verification through view abstraction. STTT 18(5), 495–516 (2016). Scholar
  5. 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. 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). Scholar
  7. 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). Scholar
  8. 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).,
  9. 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).
  10. 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).
  11. 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).
  12. 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).
  13. 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.
  14. 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). Scholar
  15. 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). Scholar
  16. 16.
    Emmi, M., Enea, C.: Sound, complete, and tractable linearizability monitoring for concurrent collections. PACMPL 2(POPL), 25:1–25:27 (2018). Scholar
  17. 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).
  18. 18.
    German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992). Scholar
  19. 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). Scholar
  20. 20.
    Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990). Scholar
  21. 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). Scholar
  22. 22.
    Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690–691 (1979). Scholar
  23. 23.
    Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978). Scholar
  24. 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).
  25. 25.
    Mahajan, P., Alvisi, L., Dahlin, M.: Consistency, availability, convergence. Technical report (2011)Google Scholar
  26. 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). Scholar
  27. 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).
  28. 28.
    Qadeer, S.: Verifying sequential consistency on shared-memory multiprocessors by model checking. IEEE Trans. Parallel Distrib. Syst. 14(8), 730–741 (2003). Scholar
  29. 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).
  30. 30.
    Wing, J.M., Gong, C.: Testing and verifying concurrent objects. J. Parallel Distrib. Comput. 17(1–2), 164–182 (1993). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Rachid Zennou
    • 1
    • 2
    Email author
  • Ranadeep Biswas
    • 1
  • Ahmed Bouajjani
    • 1
  • Constantin Enea
    • 1
  • Mohammed Erradi
    • 2
  1. 1.Université de Paris, IRIF, CNRSParisFrance
  2. 2.ENSIASUniversity Mohammed VRabatMorocco

Personalised recommendations