Abstract
Distribution of computation is well-known, and there are several frameworks, including some formal frameworks, that capture distributed computation. As yet, however, models of distributed computation are based on the idea that data is conceptually centralized. That is, they assume that data, even if it is distributed, is consistent. This assumption is not valid for many of the database systems in use today, where consistency is compromised to ensure availability and partition tolerance. Starting with an informal definition of eventual consistency, this paper explores several measures of inconsistency that quantify how far from consistency a system is. These measures capture key aspects of eventual consistency in terms of distributed abstract state machines. The definitions move from the traditional binary definition of consistency to more quantitative definitions, where the classical consistency is given by the highest possible level of consistency. Expressing eventual consistency in terms of abstract state machines allows models to be developed that capture distributed computation and highly available distributed data within a single framework.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
In the conceptually centralized model, the read and write handling is also moved out of the agent code, but it is still inside the agent activity, which is not completed until everything is sorted out.
- 2.
- 3.
- 4.
Obviously, this also implies that \(DeltaConsistencyTime > 0\).
References
Apache Software Foundation: Apache Cassandra 4.0 - Web Page and Documentation (2019). http://cassandra.apache.org/
Best, E.: Semantics of Sequential and Parallel Programs. Prentice Hall, Upper Saddle River (1996)
Blass, A., Gurevich, Y.: Ordinary interactive small-step algorithms I. ACM Trans. Comput. Logic 7(2), 363–419 (2006)
Blass, A., Gurevich, Y., Rosenzweig, D., Rossman, B.: Interactive small-step algorithms II: abstract state machines and the characterization theorem. Logical Methods Comput. Sci. 3(4) (2007). https://doi.org/10.2168/LMCS-3(4:4)2007
Blass, A., Gurevich, Y.: Persistent queries. CoRR abs/0811.0819 (2008). http://arxiv.org/abs/0811.0819
Blass, A., Gurevich, Y.: Persistent queries in the behavioral theory of algorithms. ACM Trans. Comput. Logic (TOCL) 12(2), 16:1–16:43 (2011). https://doi.org/10.1145/1877714.1877722
Börger, E., Cisternino, A. (eds.): Advances in Software Engineering. LNCS, vol. 5316. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89762-0
Börger, E., Stärk, R.: Abstract State Machines - A Method for High-Level System Design and Analysis. Springer, Berlin (2003). https://doi.org/10.1007/978-3-642-18216-7
Börger, E., Raschke, A.: Modelling Companion for Software Practitioners. Springer, Berlin (2018). https://doi.org/10.1007/978-3-662-56641-1
Börger, E., Schewe, K.D.: Concurrent abstract state machines. Acta Inf. 53(5), 469–492 (2016). https://doi.org/10.1007/s00236-015-0249-7
Bosneag, A.M., Brockmeyer, M.: A unified formal specification for a multi-consistency replication system for DHTs. In: 12th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS 2005), pp. 33–40. IEEE (2005)
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
Bouajjani, A., Enea, C., Hamza, J.: Verifying eventual consistency of optimistic replication systems. ACM SIGPLAN Not. 49(1), 285–296 (2014). https://doi.org/10.1145/2578855.2535877
Brewer, E.A.: Towards robust distributed systems (abstract). In: Proceedings of the Nineteenth Annual ACM Symposium on Principles of Distributed Computing, PODC 2000, p. 7. ACM, New York (2000). https://doi.org/10.1145/343477.343502
Burkhardt, S.: Principles of eventual consistency. Found. Trends Program. Lang. 1, 1–150 (2014)
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978). https://doi.org/10.1145/359576.359585
ITU-T: Specification And Description Language SDL (Z.100 Series). International standard, International Telecommunication Union, Telecommunication Standardization Sector (2016–2018)
ITU-T: Specification and Description Language – Overview of SDL-2010, Annex F1: SDL-2010 formal definition: General overview. International standard, International Telecommunication Union, Telecommunication Standardization Sector (2016–2018)
Manson, J., Pugh, W., Adve, S.V.: The Java memory model. SIGPLAN Not. 40(1), 378–391 (2005). https://doi.org/10.1145/1047659.1040336
Mills, D.L.: A brief history of NTP time: memoirs of an internet timekeeper. SIGCOMM Comput. Commun. Rev. 33(2), 9–21 (2003). https://doi.org/10.1145/956981.956983
Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10235-3
Mironov, A.M.: Theory of processes. CoRR abs/1009.2259 (2010). http://arxiv.org/abs/1009.2259
Object Management Group (OMG): OMG® Unified Modeling Language® (OMG UML®), Version 2.5.1. OMG Document Number formal, 05 December 2017. http://www.omg.org/spec/UML/2.5.1
Prinz, A.: Distributed computing on distributed memory. In: Khendek, F., Gotzhein, R. (eds.) SAM 2018. LNCS, vol. 11150, pp. 67–84. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01042-3_5
Prinz, A., Sherratt, E.: Distributed ASM - pitfalls and solutions. In: Aït-Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 210–215. Springer, Berlin (2014). https://doi.org/10.1007/978-3-662-43652-3_18
Schewe, K., Prinz, A., Börger, E.: Concurrent computing with shared replicated memory. CoRR abs/1902.04789 (2019). http://arxiv.org/abs/1902.04789
Sherratt, E.: Relativity and abstract state machines. In: Haugen, Ø., Reed, R., Gotzhein, R. (eds.) SAM 2012. LNCS, vol. 7744, pp. 105–120. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36757-1_7
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Sherratt, E., Prinz, A. (2019). Eventual Consistency Formalized. In: Fonseca i Casas, P., Sancho, MR., Sherratt, E. (eds) System Analysis and Modeling. Languages, Methods, and Tools for Industry 4.0. SAM 2019. Lecture Notes in Computer Science(), vol 11753. Springer, Cham. https://doi.org/10.1007/978-3-030-30690-8_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-30690-8_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30689-2
Online ISBN: 978-3-030-30690-8
eBook Packages: Computer ScienceComputer Science (R0)