Foundations and Trends® in Programming Languages > Vol 1 > Issue 1-2

Principles of Eventual Consistency

By Sebastian Burckhardt, Microsoft Research, USA, sburckha@microsoft.com

 
Suggested Citation
Sebastian Burckhardt (2014), "Principles of Eventual Consistency", Foundations and Trends® in Programming Languages: Vol. 1: No. 1-2, pp 1-150. http://dx.doi.org/10.1561/2500000011

Publication Date: 09 Oct 2014
© 2014 S. Burckhardt
 
Subjects
Parallel and Distributed Database Systems,  Peer-to-Peer, Sensornet and Mobile Data Management,  Distributed computing
 

Free Preview:

Download extract

Share

Login to download a free copy
In this article:
1. Introduction 
2. Preliminaries 
3. Consistency Specifications 
4. Replicated Data Types 
5. Consistency 
6. Implementations 
7. Concrete Executions 
8. Protocols 
9. Implementability 
10. Correctness 
11. Related Work 
12. Conclusion 
Acknowledgements 
Appendices 
References 

Abstract

In globally distributed systems, shared state is never perfect. When communication is neither fast nor reliable, we cannot achieve strong consistency, low latency, and availability at the same time. Unfortunately, abandoning strong consistency has wide ramifications. Eventual consistency, though attractive from a performance viewpoint, is challenging to understand and reason about, both for system architects and programmers. To provide robust abstractions, we need not just systems, but also principles: we need the ability to articulate what a consistency protocol is supposed to guarantee, and the ability to prove or refute such claims.

In this tutorial, we carefully examine both the what and the how of consistency in distributed systems. First, we deconstruct consistency into individual guarantees relating the data type, the conflict resolution, and the ordering, and then reassemble them into a hierarchy of consistency models that starts with linearizability and gradually descends into sequential, causal, eventual, and quiescent consistency. Second, we present a collection of consistency protocols that illustrate common techniques, and include templates for implementations of arbitrary replicated data types that are fully available under partitions. Third, we demonstrate that our formalizations serve their purpose of enabling proofs and refutations, by proving both positive results (the correctness of the protocols) and a negative result (a version of the CAP theorem for sequential consistency).

DOI:10.1561/2500000011
ISBN: 978-1-60198-858-4
170 pp. $99.00
Buy book (pb)
 
ISBN: 978-1-60198-859-1
170 pp. $240.00
Buy E-book (.pdf)
Table of contents:
1. Introduction
2. Preliminaries
3. Consistency Specifications
4. Replicated Data Types
5. Consistency
6. Implementations
7. Concrete Executions
8. Protocols
9. Implementability
10. Correctness
11. Related Work
12. Conclusion
Acknowledgements
Appendices
References

Principles of Eventual Consistency

In globally distributed systems, shared state is never perfect. When communication is neither fast nor reliable, it is not possible to achieve strong consistency, low latency, and availability at the same time. Unfortunately, abandoning strong consistency has wide ramifications. Eventual consistency, though attractive from a performance viewpoint, is challenging to understand and reason about for both system architects and programmers. To provide robust abstractions, we need not just systems but also principles; we need the ability to articulate what a consistency protocol is supposed to guarantee, and the ability to prove or refute such claims.

Principles of Eventual Consistency carefully examines both the what and the how of consistency in distributed systems. It provides the reader with tools for reasoning about consistency of protocols. The emphasis is on using basic mathematical techniques, such as sets, relations, and first order logic, to describe a wide variety of consistency guarantees, and to define protocols with a level of precision that enables us to prove both positive results – correctness of protocols – and negative results – refute implementability.

 
PGL-011