Crate cvrdt_exposition

source ·
Expand description

Understanding Convergent Replicated Data Types

I wanted to understand CRDTs more, so I put together this Rust library for state-based CRDTs a.k.a. convergent replicated data types a.k.a. CvRDTs. It aims to present an explicit (with strong types, etc.) and unified description of the CvRDTs presented in the wonderful paper A comprehensive study of Convergent and Commutative Replicated Data Types.

Do not use this!

This code is solely for my own edification and is not meant for production use. There are already much better options for usable CRDTs in Rust; see the rust-crdt project.

What makes a CvRDT?

Quoting the Wikipedia article on CRDTs,

CvRDTs send their full local state to other replicas, where the states are merged by a function which must be commutative, associative, and idempotent.

So suppose we’ve just written a brand new data type, and we’d like to demonstrate it’s a CvRDT. Suppose further that x, y, and z are any arbitrary members of our data type, and that our data type has a merge function called merge; for our type to be a CvRDT, we need the following three things to be true for any values of x, y, and z:

  1. merge(x, y) = merge(y, x)
  2. merge(x, merge(y, z)) = merge(merge(x, y), z)
  3. merge(merge(x, y), y) = merge(x, y)

Wikipedia continues,

The merge function provides a join for any pair of replica states, so the set of all states forms a semilattice.

Our merge function merge induces a partial order on all the elements of our type, akin to Rust’s PartialOrd trait, where x ≤ y if merge(x, y) = y. Since for any two elements x and y, both x ≤ merge(x, y) and y ≤ merge(x, y), and merge(x, y) is the “smallest” such elment for which this occurs, it is the least upper bound (or join) of x and y.

The article goes on

The update function must monotonically increase the internal state, according to the same partial order rules as the semilattice.

Suppose our type has an update function which we’ll call add. For any element x and update value u, we need x ≤ update(x, u); that is, we need merge(x, update(x, u)) = update(x, u).

Many types of CvRDT—in this library especially—are grow-only; they can add new elements/values/etc., but once added, these cannot be removed. Some types allow removal as well; if our type does so, we must ensure that removal maintains the partial order given by our merge function. That is, we need the internal state to increase monotonically (as Wikipedia says in the above quote) even in the face of removals. Suppose our type has a function

Ideally we’d check these requirements for every possible configuration of our new CvRDT implementation. This can be impossible to do via brute force, as the number of states to check can quickly get prohibitively large. See the penultimate section for how cvrdt-exposition verifies these properties.

Examples

Per the Wikipedia article, consider a one-way boolean flag that, once true, can never revert to false:

use cvrdt_exposition::{Grow, OneWayBoolean};
let x = OneWayBoolean::new(false);
let mut y = OneWayBoolean::new(false);
y.add(());
assert_eq!(y.payload(), true);
assert_eq!(y.merge(&x).payload(), true);

As the internal state of a OneWayBoolean is only a single boolean value, we could verify the implementation fulfills the CvRDT requirements by hand (though I’d rather get my computer to do it! see below).

How cvrdt-exposition verifies properties

In the absence of using formal methods like TLA+ (see also Hillel Wayne’s excellent book!), we resort to property-based testing via the proptest crate. This excellent crate is listed as a dev-dependency in cvrdt-exposition’s Cargo.tml file, so if you can just use the stuff in this library (although you shouldn’t!) without pulling in an extra dependency. That said, I highly recommend learning to use proptest, quickcheck, or some other property testing framework for Rust.

In the cfg(test)-only properties module, cvrdt-exposition defines macros for automating checking CvRDT properties. For instance, given a function arb_cvrdt2 that yields an arbitrary pair of elements of our CvRDT type, proptest’s proptest! macro allows us to test that our CvRDT’s merge function is commutative via:

ⓘ
proptest! {
    #[test]
    fn merge_commutative((x, y) in $arb_cvrdt2()) {
        prop_assert_eq!(
            Grow::payload(&Grow::merge(&x, &y)),
            Grow::payload(&Grow::merge(&y, &x))
        );
    }
};

Note that the above code uses the cvrdt-exposition nomenclature Grow, which we use to distinguish CvRDTs that are grow-only from those that can also remove elements. See the traits documentation for more.

References

Re-exports

Modules