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 that you have read and understand our privacy policy and code of conduct.