Verifying Strong Eventual Consistency in $\delta$-CRDTs

TL;DR

This paper formalizes and proves that $ ext{delta}$-state CRDTs maintain strong eventual consistency even with minimal communication and weak network assumptions, making them suitable for real-world distributed systems.

Contribution

It provides a formal proof in Isabelle that $ ext{delta}$-state CRDTs achieve SEC under relaxed network conditions, extending the understanding of their robustness.

Findings

$ ext{delta}$-state CRDTs require less communication overhead.

They maintain SEC under weak network assumptions.

Formal proofs are provided in Isabelle for these properties.

Abstract

Conflict-free replicated data types (CRDTs) are a natural structure with which to communicate information about a shared computation in a distributed setting where coordination overhead may not be tolerated, and individual participants are allowed to temporarily diverge from the overall computation. Within this setting, there are two classical approaches: state- and operation-based CRDTs. The former define a commutative, associative, and idempotent join operation, and their states a monotone join semi-lattice. State-based CRDTs may be further distinguished into classical- and $\delta$-state CRDTs. The former communicate their full state after each update, whereas the latter communicate only the changed state. Op-based CRDTs communicate operations (not state), thus making their updates non-idempotent. Whereas op-based CRDTs require little information to be exchanged, they demand relatively strong network guarantees (exactly-once message delivery), and state-based CRDTs suffer the opposite problem. Both satisfy strong eventual consistency (SEC). We posit that $\delta$-state CRDTs both (1) require less communication overhead from payload size, and (2) tolerate relatively weak network environments, making them an ideal candidate for real-world use of CRDTs. Our central intuition is a pair of reductions between state-, $\delta$-state, and op-based CRDTs. We formalize this intuition in the Isabelle interactive theorem prover and show that state-based CRDTs achieve SEC. We present a relaxed network model in Isabelle and show that state-based CRDTs still maintain SEC. Finally, we extend our work to show that $\delta$-state CRDTs maintain SEC when only communicating $\delta$-state fragments, even under relatively weak network conditions.