PWL Dec 2023: "Verifying Strong Eventual Consistency in Distributed Systems"

About the paper

Data replication is a well discussed concept for maintaining up-to-date copies of shared data in distributed systems. Although it is critical for the correctness of a system, implementing it still remains a challenging task. Despite decades of research, achieving consistency in replicated systems is still not well understood, in fact, many previously published algorithms have been later shown to be incorrect.

If we have to prove the correctness of Conflict-Free Replicated Datatypes, we need to formalise the guarantees it provides - Strong Eventual Consistency (SEC), and we have to do this in the context of a network-model that reflects real-world computer networks, with all the asynchronous and unreliable goodness modeled in as well.

The paper builds step by step towards this goal of formalising SEC and then embedding various replication algorithms into this axiomatic network model. This is done using Isabelle/HOL, which is a strict, type-inferred proof assistant.

The paper is published here: https://www.cl.cam.ac.uk/~arb33/papers/GomesEtAl-VerifyingSEC-OOPSLA2017.pdf

Key Takeaways

• Basic definitions and some necessary conditions for replication algorithms, a great read to understand concepts like SEC and what it guarantees, and causality in the context of generalised network models
• How we can move step-by-step defining conditions, locales and theorems for some really subtle concepts using Isabelle/HOL. Even if you are new to Formal Methods, the approach this paper takes explaining it is intuitive.
• Defining an axiomatic network model that doesn’t make wrong assumptions about the real-world and embedding some simple replication algorithms like RGA, Counter and OR-Set

About the Presenter

Raghav Roy is a systems engineer at VMware working with Network Virtualisation and the ESXi kernel. His interests (atleast relevant to this paper) include distributed systems, formalisation techniques and its application in real world systems, and building systems that scale.
He also contributes to open source, which is mostly Kubernetes, but the struggle with maintaining closed source and open source contributions is something he is very vocal about.

Slides for this talk: https://speakerdeck.com/royra/pwl-dec-2023-verifying-strong-eventual-consistency-in-distributed-systems