Ahmed Bouajjani
ABSTRACT
Causal consistency is one of the most adopted consistency criteria for distributed implementations of data structures. It ensures that operations are executed at all sites according to their causal precedence. We address the issue of verifying automatically whether the executions of an implementation of a data structure are causally consistent. We consider two problems: (1) checking whether one single execution is causally consistent, which is relevant for developing testing and bug finding algorithms, and (2) verifying whether all the executions of an implementation are causally consistent.
We show that the first problem is NP-complete. This holds even for the read-write memory abstraction, which is a building block of many modern distributed systems. Indeed, such systems often store data in key-value stores, which are instances of the read-write memory abstraction. Moreover, we prove that, surprisingly, the second problem is undecidable, and again this holds even for the read-write memory abstraction. However, we show that for the read-write memory abstraction, these negative results can be circumvented if the implementations are data independent, i.e., their behaviors do not depend on the data values that are written or read at each moment, which is a realistic assumption.
We prove that for data independent implementations, the problem of checking the correctness of a single execution w.r.t. the read-write memory abstraction is polynomial time. Furthermore, we show that for such implementations the set of non-causally consistent executions can be represented by means of a finite number of register automata. Using these machines as observers (in parallel with the implementation) allows to reduce polynomially the problem of checking causal consistency to a state reachability problem. This reduction holds regardless of the class of programs used for the implementation, of the number of read-write variables, and of the used data domain. It allows leveraging existing techniques for assertion/reachability checking to causal consistency verification. Moreover, for a significant class of implementations, we derive from this reduction the decidability of verifying causal consistency w.r.t. the read-write memory abstraction.
- P. A. Abdulla, F. Haziza, L. Hol´ık, B. Jonsson, and A. Rezine. An integrated specification and verification technique for highly concurrent data structures. In TACAS ’13. Springer, 2013. Google Scholar
Digital Library
- M. Ahamad, G. Neiger, J. E. Burns, P. Kohli, and P. W. Hutto. Causal memory: definitions, implementation, and programming. Distributed Computing, 9(1):37–49, 1995.Google ScholarDigital Library
- R. Alur, K. L. McMillan, and D. Peled. Model-checking of correctness conditions for concurrent objects. Inf. Comput., 160(1-2), 2000. Google ScholarDigital Library
- M. F. Atig, A. Bouajjani, and T. Touili. Analyzing asynchronous programs with preemption. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008, December 9-11, 2008, Bangalore, India, pages 37–48, 2008.Google Scholar
- P. Bailis, A. Ghodsi, J. M. Hellerstein, and I. Stoica. Bolt-on causal consistency. In SIGMOD ’13, pages 761–772, New York, NY, USA, 2013. ACM. Google ScholarDigital Library
- L. Benmouffok, J.-M. Busca, J. M. Marquès, M. Shapiro, P. Sutra, and G. Tsoukalas. Telex: A semantic platform for cooperative application development. In CFSE, Toulouse, France, 2009.Google Scholar
- K. P. Birman. Replication and fault-tolerance in the ISIS system, volume 19. ACM, 1985.Google ScholarDigital Library
- A. Bouajjani, C. Enea, and J. Hamza. Verifying eventual consistency of optimistic replication systems. In POPL ’14, pages 285–296, New York, NY, USA, 2014. ACM. Google ScholarDigital Library
- A. Bouajjani, M. Emmi, C. Enea, and J. Hamza. On reducing linearizability to state reachability. In ICALP ’15, pages 95–107. Springer, 2015. Google ScholarDigital Library
- A. Bouajjani, C. Enea, R. Guerraoui, and J. Hamza. On Verifying Causal Consistency. ArXiv e-prints, Nov. 2016.Google Scholar
- P. Bouyer, A. Petit, and D. Thérien. An algebraic characterization of data and timed languages. In K. G. Larsen and M. Nielsen, editors, CONCUR 2001 - Concurrency Theory, 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings, volume 2154 of Lecture Notes in Computer Science, pages 248–261. Springer, 2001. Google ScholarDigital Library
- S. Burckhardt. Principles of Eventual Consistency. now publishers, October 2014. Google ScholarDigital Library
- S. Burckhardt, A. Gotsman, and H. Yang. Understanding eventual consistency. Technical Report MSR-TR-2013-39, Microsoft Research.Google Scholar
- J. Du, S. Elnikety, A. Roy, and W. Zwaenepoel. Orbe: scalable causal consistency using dependency matrices and physical clocks. In ACM Symposium on Cloud Computing, SOCC ’13, Santa Clara, CA, USA, October 1-3, 2013, pages 11:1–11:14, 2013. Google ScholarDigital Library
- J. Du, C. Iorgulescu, A. Roy, and W. Zwaenepoel. Gentlerain: Cheap and scalable causal consistency with physical clocks. In Proceedings of the ACM Symposium on Cloud Computing, Seattle, WA, USA, November 03 - 05, 2014, pages 4:1–4:13, 2014. Google ScholarDigital Library
- J. Esparza. Decidability and complexity of petri net problems — an introduction. In Lectures on Petri Nets I: Basic Models. Springer Berlin Heidelberg, 1998. Google ScholarDigital Library
- C. J. Fidge. Timestamps in message-passing systems that preserve the partial ordering. Australian National University. Department of Computer Science, 1987.Google Scholar
- M. J. Fischer, N. A. Lynch, and M. S. Paterson. Impossibility of distributed consensus with one faulty process. J. ACM, 32(2):374– 382, Apr. 1985. Google ScholarDigital Library
- F. Furbach, R. Meyer, K. Schneider, and M. Senftleben. Memory model-aware testing - a unified complexity analysis. In Application of Concurrency to System Design (ACSD), 2014 14th International Conference on, pages 92–101, June 2014. Google ScholarDigital Library
- S. Gilbert and N. A. Lynch. Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News, 33(2):51–59, 2002. Google ScholarDigital Library
- J. Hamza. Algorithmic Verification of Concurrent and Distributed Data Structures. PhD thesis, Université Paris Diderot, 2015.Google Scholar
- J. Hamza. On the complexity of linearizability. In NETYS ’15, volume 9466 of Lecture Notes in Computer Science. Springer, 2015.Google Scholar
- T. A. Henzinger, A. Sezgin, and V. Vafeiadis. Aspect-oriented linearizability proofs. In CONCUR ’13. Springer, 2013. Google ScholarDigital Library
- M. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3), 1990. Google ScholarDigital Library
- J. Hopcroft and J.-J. Pansiot. On the reachability problem for 5dimensional vector addition systems. Theoretical Computer Science, 8(2):135–159, 1979.Google ScholarCross Ref
- E. Jiménez, A. Fernández, and V. Cholvi. A parametrized algorithm that implements sequential, causal, and cache memory consistencies. J. Syst. Softw., 81(1):120–131, Jan. 2008. ISSN 0164-1212. Google ScholarDigital Library
- R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and system Sciences, 3(2):147–195, 1969. Google ScholarDigital Library
- A.-M. Kermarrec, A. I. T. Rowstron, M. Shapiro, and P. Druschel. The icecube approach to the reconciliation of divergent replicas. In PODC, pages 210–218, 2001. Google ScholarDigital Library
- R. Ladin, B. Liskov, L. Shrira, and S. Ghemawat. Providing high availability using lazy replication. ACM Trans. Comput. Syst., 10(4): 360–391, Nov. 1992. ISSN 0734-2071. Google ScholarDigital Library
- L. Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558–565, July 1978. Google ScholarDigital Library
- L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput., 28(9):690– 691, Sept. 1979. ISSN 0018-9340. Google ScholarDigital Library
- M. Lesani, C. J. Bell, and A. Chlipala. Chapar: certified causally consistent distributed key-value stores. In ACM SIGPLAN Notices, volume 51, pages 357–370. ACM, 2016. Google ScholarDigital Library
- W. Lloyd, M. J. Freedman, M. Kaminsky, and D. G. Andersen. Don’t settle for eventual: scalable causal consistency for wide-area storage with COPS. In SOSP, pages 401–416, 2011. Google ScholarDigital Library
- F. Mattern. Virtual time and global states of distributed systems. In PARALLEL AND DISTRIBUTED ALGORITHMS, pages 215–226. North-Holland, 1988.Google Scholar
- J. Michaux, X. Blanc, M. Shapiro, and P. Sutra. A semantically rich approach for collaborative model edition. In SAC, pages 1470–1475, 2011. Google ScholarDigital Library
- M. Perrin, A. Mostefaoui, and C. Jard. Causal consistency: Beyond memory. In Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP ’16, pages 26:1–26:12, New York, NY, USA, 2016. ACM. ISBN 978-1-4503- 4092-2. Google ScholarDigital Library
- C. A. Petri. Kommunikation mit automaten. 1962.Google Scholar
- M. Raynal and A. Schiper. From causal consistency to sequential consistency in shared memory systems. In International Conference on Foundations of Software Technology and Theoretical Computer Science, pages 180–194. Springer, 1995. Google ScholarDigital Library
- D. B. Terry, A. J. Demers, K. Petersen, M. Spreitzer, M. Theimer, and B. W. Welch. Session guarantees for weakly consistent replicated data. In Proceedings of the Third International Conference on Parallel and Distributed Information Systems, PDIS ’94, pages 140–149, Washington, DC, USA, 1994. IEEE Computer Society. ISBN 0-8186-6400-2. Google ScholarDigital Library
- D. B. Terry, M. Theimer, K. Petersen, A. J. Demers, M. Spreitzer, and C. Hauser. Managing update conflicts in bayou, a weakly connected replicated storage system. In M. B. Jones, editor, Proceedings of the Fifteenth ACM Symposium on Operating System Principles, SOSP 1995, Copper Mountain Resort, Colorado, USA, December 3-6, 1995, pages 172–183. ACM, 1995. Google ScholarDigital Library
- D. B. Terry, V. Prabhakaran, R. Kotla, M. Balakrishnan, M. K. Aguilera, and H. Abu-Libdeh. Consistency-based service level agreements for cloud storage. In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, SOSP ’13, pages 309–324, New York, NY, USA, 2013. ACM. ISBN 978-1-4503-2388-8. Google ScholarDigital Library
- H. Wei, Y. Huang, J. Cao, X. Ma, and J. Lu. Verifying PRAM consistency over read/write traces of data replicas. CoRR, abs/1302.5161, 2013.Google Scholar
- P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In POPL ’86: Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, pages 184–193. ACM Press, 1986. Google ScholarDigital Library
- M. Zawirski, N. Preguic¸a, S. Duarte, A. Bieniusa, V. Balegas, and M. Shapiro. Write fast, read in the past: Causal consistency for clientside applications. In Proceedings of the 16th Annual Middleware Conference, Middleware ’15, pages 75–87, New York, NY, USA, 2015. ACM. ISBN 978-1-4503-3618-5. Google ScholarDigital Library
Index Terms
- On verifying causal consistency
Recommendations
Causal consistency: beyond memory
PPoPP '16: Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel ProgrammingIn distributed systems where strong consistency is costly when not impossible, causal consistency provides a valuable abstraction to represent program executions as partial orders. In addition to the sequential program order of each computing entity, ...
On verifying causal consistency
POPL '17Causal consistency is one of the most adopted consistency criteria for distributed implementations of data structures. It ensures that operations are executed at all sites according to their causal precedence. We address the issue of verifying ...
Verifying eventual consistency of optimistic replication systems
POPL '14We address the verification problem of eventual consistency of optimistic replication systems. Such systems are typically used to implement distributed data structures over large scale networks. We introduce a formal definition of eventual consistency ...
Comments