Advertisement

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)

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.

References

  1. 1.
    https://www.cockroachlabs.com. Accessed 15 Nov 2018
  2. 2.
    http://galeracluster.com. 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).  https://doi.org/10.1007/s10009-015-0406-xCrossRefGoogle 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).  https://doi.org/10.1007/BF01784241MathSciNetCrossRefGoogle 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).  https://doi.org/10.1006/inco.1999.2847MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1145/2463676.2465279, http://doi.acm.org/10.1145/2463676.2465279
  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). http://dl.acm.org/citation.cfm?id=3009888
  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).  https://doi.org/10.1145/2535838.2535877. http://doi.acm.org/10.1145/2535838.2535877
  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).  https://doi.org/10.1145/1806596.1806634
  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).  https://doi.org/10.1145/2523616.2523628. http://doi.acm.org/10.1145/2523616.2523628
  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.  https://doi.org/10.1145/2670979.2670983
  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).  https://doi.org/10.1007/3-540-60045-0_63CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-96145-3_26CrossRefGoogle Scholar
  16. 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/3158113CrossRefGoogle 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).  https://doi.org/10.1145/2737924.2737983
  18. 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.146681MathSciNetCrossRefGoogle 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).  https://doi.org/10.1145/564585.564601CrossRefGoogle 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).  https://doi.org/10.1145/78969.78972CrossRefGoogle 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).  https://doi.org/10.1016/j.jss.2007.03.012CrossRefGoogle Scholar
  22. 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.1675439CrossRefzbMATHGoogle Scholar
  23. 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.359563CrossRefzbMATHGoogle 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).  https://doi.org/10.1145/2043556.2043593
  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).  https://doi.org/10.1145/269005.266711CrossRefGoogle 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).  https://doi.org/10.1109/SRDSW.2014.33
  28. 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.1225053CrossRefGoogle 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).  https://doi.org/10.1145/800070.802186
  30. 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.1015MathSciNetCrossRefzbMATHGoogle 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