CRDTs for Free
Conflict-Free Replicated Data Types (CRDTs) are one of the core technical building blocks behind Ossa's secure synchronization protocol. CRDTs are special datatypes that enable data synchronization without a central server and allow users to make document edits even while offline. To provide these features, CRDTs must satisfy stringent mathematical properties.
CRDTs were formalized by Shapiro et al. and are required to guarantee Strong Eventual Consistency, which ensures that application state eventually converges between replicas once they have received the same set of update operations. CRDTs satisfy Strong Eventual Consistency by ensuring that concurrent operations commute. Here is the commutativity property stated mathematically:
def commutativity := forall st: CRDT, op1: Operation, op2: Operation,
concurrent(op1, op2) =>
st.apply(op1).apply(op2) == st.apply(op2).apply(op1)
In other words, given two concurrent operations op1 and op2, if you apply op1 and then op2 to a CRDT, its final state is the same as if you applied op2 and then op1.
As a result, application state converges to the same value, regardless of the order that updates were received.
In practice, this enables collaborative applications where devices can sync directly over peer-to-peer connections and users can update their documents while offline.
Designing data types that satisfy the required CRDT properties is nontrivial. Fortunately, there are many CRDT primitives for commonly used data structures like registers, sequences, sets, and maps. As an example, consider the simple Last Writer Wins CRDT that serves as a register.
struct LWW<Time, A> {
time: Time,
value: A,
}