Partial Order over CRDT's

[davidrusu]

Partial orders are central to all CRDT's, we should have the PartialOrder trait implemented for all CRDT's and once done, we should be able to write some more interesting tests.

ie. the merge(a, b) should be the least-upper-bound of {a, b}.

Leaving this here as a half finished thought to explore later.

[hjorvari]

I really want to write a join semi-lattice trait since that is precisely a CRDT (unique glb), a CRDT is obviously a partial order but a partial order doesn't necessarily have eventual consistency.

There is a typeclass / library for this in haskell:
https://hackage.haskell.org/package/lattices-1.5.0/docs/Algebra-Lattice.html

Any idea what the possible blockers could be for translating that library to rust? I haven't looked at the code yet, just curious if you have any input.

[davidrusu]

Well, a few things, first, a join semi-lattice is an alias for a CvRDT (state replicated CRDT), and we've already got a trait for that in this library.

Second, a trait by itself is not that interesting, you need someway of checking the laws (assoc, commute, idempotent, LUB, etc.) and writing down the trait(or typeclass) definition gets you nowhere closer to verifying an instance follows these laws. Most of the work is in testing that a CRDT's follow the CRDT laws. (Haskell doesn't help you here either)

The point of this issue was to give us one more tools for writing some more sophisticated property tests for the CRDT laws, a partial order over CRDT's would allow us to write properties like:

Let C = merge(A, B)
then C >= A and C >= B

[hjorvari]

Thank you, I knew I had to be missing something. Now this makes sense, so you want to show that CRDT implies partial order? It's obviously trivial to write the partial_cmp function since you can just do something like:

match merge(A, B) {
  A => Some(cmp::Greater)
  B => Some(cmp::Lesser)
  _ => None
}

I don't write much rust, so I may still be missing something?

Edit: that match statement would obviously be inside the definition of A.partial_cmp(&B)
Edit2: A and B are Eq so the A==B case can be handled before the match
Edit3: Okay I am now reading and playing with the code, my next comment will be better informed >,<
Edit4: Ahh I get it I think, if you define the order in terms of merge then it is useless for testing merge you want the property so that you can make sure merge is behaving correctly.

[chpio]

match merge(A, B) {
  A => Some(cmp::Greater)
  B => Some(cmp::Lesser)
  _ => None
}

do you mean?:

let ab = merge(a, b);
if ab == a {
  Some(cmp::Greater)
} else if ab == b {
  Some(cmp::Lesser)
} else {
  None
}

That would only work if one (a or b) is based on the other, but what if they diverged from one another (got different data applied to them).

edit: hmm, yes ur right... at least for:

Let C = merge(A, B)
then C >= A and C >= B

but not in a general way?

[hjorvari]

Generally; a merge of two members in a CRDT is equivalent to a join in a semilattice, this is because a CRDT requires a unique result of the merge operation (or you wouldn't have eventual consistency) and this is exactly the property that refines a partial order into a semilattice.

In mathematics when you want to show that semilattice is partially ordered you define the ordering as I did above, if A and B have diverged then there is no ordering between them.

https://ncatlab.org/nlab/show/semilattice
https://ncatlab.org/nlab/show/join

However, in a computer you need to be more paranoid I guess, so the idea is to use the inter-relation of mathematical concepts to verify that the implementation is correct (asserts).

[davidrusu]

There are many partial orders that can be defined over a structure, the one we are looking for is the partial order that induces the merge function we are using for a particular CRDT.

In math you would say that the merge of two CRDT states is defined as the least upper bound of A and B under a given partial order.

merge(A,B) = lub {A, B}

expanding just a bit, we can say:

C = merge(A, B)

C is an upper bound:

C >= A
C >= B

C is the least upper bound:

∄ x s.t. x < C and x >= A and x >= B

So the interesting thing to understand is really just that the merge function is uniquely defined by the partial order, (merge(A, B) = lub { A, B }), but this is hard to write in code, so instead of defining our CRDT in terms of lub's over partial order's directly, we skip to directly implementing merge. A side-effect is that we obscure the underlying partial order that induced this merge function.

The goal is to somehow get closer to this underlying partial order (and there is a very particular partial order we are looking for) to make sure that our merge function really does implement least-upper-bound.