Mohsen Lesani
Adam Chlipala
ABSTRACT
Today’s Internet services are often expected to stay available and render high responsiveness even in the face of site crashes and network partitions. Theoretical results state that causal consistency is one of the strongest consistency guarantees that is possible under these requirements, and many practical systems provide causally consistent key-value stores. In this paper, we present a framework called Chapar for modular verification of causal consistency for replicated key-value store implementations and their client programs. Specifically, we formulate separate correctness conditions for key-value store implementations and for their clients. The interface between the two is a novel operational semantics for causal consistency. We have verified the causal consistency of two key-value store implementations from the literature using a novel proof technique. We have also implemented a simple automatic model checker for the correctness of client programs. The two independently verified results for the implementations and clients can be composed to conclude the correctness of any of the programs when executed with any of the implementations. We have developed and checked our framework in Coq, extracted it to OCaml, and built executable stores.
- LinkedIn’s Voldemort. http://www.project-voldemort.com/.Google Scholar
- Memcached. http://memcached.org/.Google Scholar
- D. Abadi. Consistency tradeoffs in modern distributed database system design. Computer, 45(2), 2012. Google ScholarDigital Library
- M. Ahamad, G. Neiger, J. E. Burns, P. Kohli, and P. W. Hutto. Causal memory: Definitions, implementation, and programming. Distributed Computing, 9(1), 1995.Google Scholar
- H. Attiya and J. L. Welch. Sequential consistency versus linearizability. ACM Trans. Comput. Syst., 12(2), 1994. Google ScholarDigital Library
- P. Bailis, A. Ghodsi, J. M. Hellerstein, and I. Stoica. Bolt-on causal consistency. In Proc. SIGMOD, 2013. Google ScholarDigital Library
- N. Belaramani, M. Dahlin, L. Gao, A. Nayate, A. Venkataramani, P. Yalagandula, and J. Zheng. PRACTI replication. In Proc. NSDI, 2006. Google ScholarDigital Library
- M. Bickford. Component specification using event classes. In Component-Based Software Engineering, volume 5582 of Lecture Notes in Computer Science. 2009. Google ScholarDigital Library
- K. P. Birman. Replication and fault-tolerance in the ISIS system. In Proc. SOSP, 1985. Google ScholarDigital Library
- K. P. Birman and T. A. Joseph. Reliable communication in the presence of failures. ACM Trans. Comput. Syst., 5(1), 1987. Google ScholarDigital Library
- S. Bishop, M. Fairbairn, M. Norrish, P. Sewell, M. Smith, and K. Wansbrough. Engineering with logic: HOL specification and symbolicevaluation testing for TCP implementations. In Proc. POPL, 2006. Google ScholarDigital Library
- A. Bouajjani, C. Enea, and J. Hamza. Verifying eventual consistency of optimistic replication systems. In Proc. POPL, 2014. Google ScholarDigital Library
- S. Burckhardt. Principles of Eventual Consistency. Foundations and Trends in Programming Languages. 2014. Google ScholarDigital Library
- S. Burckhardt, A. Gotsman, H. Yang, and M. Zawirski. Replicated data types: Specification, verification, optimality. In Proc. POPL, 2014. Google ScholarDigital Library
- R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986. ISBN 0-13-451832-2. Google ScholarDigital Library
- B. F. Cooper, R. Ramakrishnan, U. Srivastava, A. Silberstein, P. Bohannon, H.-A. Jacobsen, N. Puz, D. Weaver, and R. Yerneni. PNUTS: Yahoo!’s hosted data serving platform. Proc. VLDB Endow., 1(2), 2008. Google ScholarDigital Library
- G. DeCandia, D. Hastorun, M. Jampani, G. Kakulapati, A. Lakshman, A. Pilchin, S. Sivasubramanian, P. Vosshall, and W. Vogels. Dynamo: Amazon’s highly available key-value store. In Proc. SOSP, 2007. Google ScholarDigital Library
- A. Gasc´on and A. Tiwari. Synthesis of a simple self-stabilizing system. In Proc. 3rd Workshop on Synthesis (SYNT), 2014.Google ScholarCross Ref
- S. Gilbert and N. Lynch. Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News, 33(2), June 2002. Google ScholarDigital Library
- Z. Guo, S. McDirmid, M. Yang, L. Zhuang, P. Zhang, Y. Luo, T. Bergan, P. Bodik, M. Musuvathi, Z. Zhang, and L. Zhou. Failure recovery: When the cure is worse than the disease. In Proc. HotOS, 2013. Google ScholarDigital Library
- M. E. Haque, Y. H. Eom, Y. He, S. Elnikety, R. Bianchini, and K. S. McKinley. Few-to-many: Incremental parallelism for reducing tail latency in interactive services. In Proc. ASPLOS, 2015. Google ScholarDigital Library
- J. He, C. A. R. Hoare, and J. W. Sanders. Data refinement refined. In Proc. ESOP, 1986. Google ScholarDigital Library
- A. John, I. Konnov, U. Schmid, H. Veith, and J. Widder. Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In Proc. FMCAD, 2013.Google ScholarCross Ref
- C. E. Killian, J. W. Anderson, R. Braud, R. Jhala, and A. M. Vahdat. Mace: Language support for building distributed systems. In Proc. PLDI, 2007. Google ScholarDigital Library
- P. Kufner, U. Nestmann, and C. Rickmann. Formal verification of distributed algorithms. In Theoretical Computer Science, volume 7604 of LNCS. 2012. Google ScholarDigital Library
- R. Ladin, B. Liskov, L. Shrira, and S. Ghemawat. Providing high availability using lazy replication. ACM Trans. Comput. Syst., 10(4), 1992. Google ScholarDigital Library
- A. Lakshman and P. Malik. Cassandra: A decentralized structured storage system. SIGOPS Oper. Syst. Rev., 44(2), 2010. Google ScholarDigital Library
- L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7), 1978. Google ScholarDigital Library
- L. Lamport. Introduction to TLA. Technical report, 1994.Google Scholar
- L. Lamport. The part-time parliament. ACM Trans. Comput. Syst., 16 (2), 1998. 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 Proc. SOSP, 2011. Google ScholarDigital Library
- W. Lloyd, M. J. Freedman, M. Kaminsky, and D. G. Andersen. Stronger semantics for low-latency geo-replicated storage. In Proc. NSDI, 2013. Google ScholarDigital Library
- N. A. Lynch and M. R. Tuttle. An introduction to input/output automata. CWI Quarterly, 2, 1989.Google Scholar
- P. Mahajan, L. Alvisi, and M. Dahlin. Consistency, availability, and convergence. Technical Report UTCS TR-11-22, The University of Texas at Austin, 2011.Google Scholar
- P. J. Marandi, S. Benz, F. Pedone, and K. P. Birman. The performance of Paxos in the cloud. In Proc. SRDS, 2014. Google ScholarDigital Library
- M. Musuvathi and D. R. Engler. Model checking large network protocol implementations. In Proc. NSDI, 2004. Google ScholarDigital Library
- K. Petersen, M. J. Spreitzer, D. B. Terry, M. M. Theimer, and A. J. Demers. Flexible update propagation for weakly consistent replication. In Proc. SOSP, 1997. Google ScholarDigital Library
- F. Pfenning and C. Elliot. Higher-order abstract syntax. In Proc. PLDI, 1988. Google ScholarDigital Library
- F. Pfenning and R. J. Simmons. Substructural operational semantics as ordered logic programming. In Proc. LICS, 2009. Google ScholarDigital Library
- G. D. Plotkin. The origins of structural operational semantics. In Proc. Journal of Logic and Algebraic Programming, pages 60–61, 2004.Google Scholar
- V. Rahli. Interfacing with proof assistants for domain specific programming using EventML. 10th International Workshop on User Interfaces for Theorem Provers, 2012.Google Scholar
- M. Raynal and A. Schiper. From causal consistency to sequential consistency in shared memory systems. volume 1026 of LNCS. 1995. Google ScholarDigital Library
- T. Ridge. Verifying distributed systems: the operational approach. In Proc. POPL, 2009. Google ScholarDigital Library
- H.-G. Roh, M. Jeon, J.-S. Kim, and J. Lee. Replicated abstract data types: Building blocks for collaborative applications. J. Parallel Distrib. Comput., 71(3), 2011. Google ScholarDigital Library
- N. Schiper, V. Rahli, R. van Renesse, M. Bickford, and R. Constable. Developing correctly replicated databases using formal tools. In Proc. DSN, 2014. Google ScholarDigital Library
- M. Shapiro, N. Preguica, C. Baquero, and M. Zawirski. A comprehensive study of Convergent and Commutative Replicated Data Types. Technical Report RR-7506, INRIA, 2011.Google ScholarDigital Library
- D. B. Terry, M. M. Theimer, K. Petersen, A. J. Demers, M. J. Spreitzer, and C. H. Hauser. Managing update conflicts in Bayou, a weakly connected replicated storage system. In Proc. SOSP, 1995. Google ScholarDigital Library
- W. Vogels. Eventually consistent. Queue, 6(6), 2008. Google ScholarDigital Library
- J. R. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang, M. D. Ernst, and T. Anderson. Verdi: A framework for implementing and formally verifying distributed system. In Proc. PLDI, 2015. Google ScholarDigital Library
- M. Yabandeh, N. Knezevic, D. Kostic, and V. Kuncak. CrystalBall: Predicting and preventing inconsistencies in deployed distributed systems. In Proc. NSDI, 2009. Google ScholarDigital Library
- J. Yang, T. Chen, M. Wu, Z. Xu, X. Liu, H. Lin, M. Yang, F. Long, L. Zhang, and L. Zhou. Modist: Transparent model checking of unmodified distributed systems. In Proc. NSDI, 2009. Google ScholarDigital Library
- D. Yuan, Y. Luo, X. Zhuang, G. R. Rodrigues, X. Zhao, Y. Zhang, P. U. Jain, and M. Stumm. Simple testing can prevent most critical failures: An analysis of production failures in distributed data-intensive systems. In Proc. OSDI, 2014. Google ScholarDigital Library
- P. Zave. Using lightweight modeling to understand Chord. SIGCOMM Comput. Commun. Rev., 42(2). Google ScholarDigital Library
- P. Zeller, A. Bieniusa, and A. Poetzsch-Heffter. Formal specification and verification of CRDTs. volume 8461 of LNCS. 2014.Google Scholar
Index Terms
- Chapar: certified causally consistent distributed key-value stores
Recommendations
Chapar: certified causally consistent distributed key-value stores
POPL '16Today’s Internet services are often expected to stay available and render high responsiveness even in the face of site crashes and network partitions. Theoretical results state that causal consistency is one of the strongest consistency guarantees that ...
Decidable verification under a causally consistent shared memory
PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and ImplementationCausal consistency is one of the most fundamental and widely used consistency models weaker than sequential consistency. In this paper, we study the verification of safety properties for finite-state concurrent programs running under a causally ...
What’s Decidable About Causally Consistent Shared Memory?
While causal consistency is one of the most fundamental consistency models weaker than sequential consistency, the decidability of safety verification for (finite-state) concurrent programs running under causally consistent shared memories is still ...
Comments