cs.DC
Verifying Strong Eventual Consistency in delta CRDTs. 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.