Ahmed Bouajjani
ABSTRACT
We 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 that applies to a wide class of existing implementations, including the ones using speculative executions. Then, we reduce the problem of checking eventual consistency to reachability and model checking problems. This reduction enables the use of existing verification tools for message-passing programs in the context of verifying optimistic replication systems. Furthermore, we derive from these reductions decision procedures for checking eventual consistency of systems implemented as finite-state programs communicating through unbounded unordered channels.
Supplemental Material
- R. Alur, K. L. McMillan, and D. Peled. Model-checking of correctness conditions for concurrent objects. Inf. Comput., 160(1-2):167--188, 2000. Google Scholar
Digital 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
- A.-M. Bosneag and M. Brockmeyer. A formal model for eventual consistency semantics. In IASTED PDCS, pages 204--209, 2002.Google Scholar
- A. Bouajjani and P. Habermehl. Constrained properties, semilinear systems, and petri nets. In CONCUR, pages 481--497, 1996. Google ScholarDigital Library
- A. Bouajjani, M. Emmi, C. Enea, and J. Hamza. Verifying concurrent programs against sequential specifications. In ESOP, 2013. Google ScholarDigital Library
- S. Burckhardt, A. Gotsman, and H. Yang. Understanding eventual consistency. Technical Report MSR-TR-2013-39, Microsoft Research.Google Scholar
- 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 SOSP, 2007. Google ScholarDigital Library
- A. Farzan and P. Madhusudan. Monitoring atomicity in concurrent programs. In CAV 2008, pages 52--65. Springer. Google ScholarDigital Library
- A. Fekete, D. Gupta, V. Luchangco, N. A. Lynch, and A. A. Shvartsman. Eventually-serializable data services. In PODC, pages 300--309, 1996. 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
- T. A. Henzinger, S. Qadeer, and S. K. Rajamani. Verifying sequential consistency on shared-memory multiprocessor systems. In CAV, volume 1633 of LNCS, pages 301--315, 1999. Google ScholarDigital Library
- M. Herlihy and N. Shavit. The art of multiprocessor programming.Google Scholar
- M. Herlihy and J. M.Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463--492, 1990. Google ScholarDigital Library
- J. H. Howard, M. L. Kazar, S. G. Menees, D. A. Nichols, M. Satyanarayanan, R. N. Sidebotham, and M. J. West. Scale and performance in a distributed file system. ACM Trans. Comput. Syst., 6(1):51--81, 1988. Google ScholarDigital Library
- P. R. Johnson and R. H. Thomas. The maintenance of duplicate databases. Technical Report Internet Request for Comments RFC 677, Information Sciences Institute, January 1976. 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
- 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
- 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
- Y. Saito and M. Shapiro. Optimistic replication. ACM Comput. Surv., 37(1):42--81, 2005. Google ScholarDigital Library
- M. Shapiro, N. Preguiça, C. Baquero, and M. Zawirski. A comprehensive study of Convergent and Commutative Replicated Data Types. Rapport de recherche RR-7506, INRIA, Jan. 2011.Google Scholar
- M. Shapiro, N. M. Preguiça, C. Baquero, and M. Zawirski. Conflict-free replicated data types. In SSS, pages 386--400, 2011. Google ScholarDigital Library
- O. Sinnen. Task Scheduling for Parallel Systems. 2007. 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. SIGOPS Oper. Syst. Rev., 29(5): 172--182, Dec. 1995. Google ScholarDigital Library
- R. Valk and M. Jantzen. The residue of vector sets with applications to decidability problems in petri nets. Acta Inf., 21:643--674, 1985.Google ScholarCross Ref
Index Terms
- Verifying eventual consistency of optimistic replication systems
Recommendations
Verifying strong eventual consistency in distributed systems
Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly ...
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 ...
On verifying causal consistency
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesCausal 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 ...
Comments