Conflict-Free Replicated Datatypes (CRDTs) are a class of distributed data structures where replica states are allowed to temporarily diverge, but will eventually converge (in the absence of network partitions). 2

Specifically, the class of CRDTs known as state-based (or convergent) achieved the above by requiring the data structure state to be drawn from a (semi)lattice (thus drawing on properties of least upper bound to achieve convergence).

Causal consistency is a consistency model where events/operations are applied in an order that is consistent with Lamport's happens-before relation. 3

Is there a formal proof that state-based CRDTs are, by construction, causally consistent?

This is hinted at in this paper 4, but without a full proof (or a full theorem statement, for that matter):

paper screenshot



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.