A framework for establishing Strong Eventual Consistency for Conflict-free Repli...
source link: https://martin.kleppmann.com/2017/07/07/isabelle-crdt-proof.html
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes
Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford
Archive of Formal Proofs, July 2017.
Abstract
In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework for verifying the correctness of CRDT algorithms. We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours. Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks. Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency. We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter.
Recommend
-
12
2017-03-03 / Event Sourcing / 10 min read Event Sourcing: Eventual Consistency and Responding to Events
-
11
Abstract 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 achievi...
-
7
Eventual Consistency isn't for Streaming This post is originally available at the Materialize blog. Streaming systems consume inputs and produce out...
-
9
[Submitted on 1 Dec 2020] Byzantine Eventual Consistency and the Fundamental Limits of Peer-to-Peer Databases Download PDF
-
5
Nebula Graph has just released v.2.6. In this version, TOSS is certainly one of the important features. Here a detailed explanation about TOSS will be given. Let’s start from a GO statement As we all know, there are t...
-
7
Eventual Consistency is a UX Nightmare Skip to main content Sponsorship available! If you'd like to sponsor CodeOpinion.com and...
-
8
HashiCorp Vault Improves Eventual Consistency with Server-Side Consistent Tokens May 26, 2022...
-
6
...
-
5
Finding and fixing eventual consistency with Stripe events Anthony Accomazzo Mar 23, 2023
-
5
Eventual Consistency in MicroservicesWhy Eventual Consistency is Highly Beneficial and How to Achieve It
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK