A few weeks ago, I gave a lightning talk at Basho’s distributed systems conference in New York, RICON|East focused around the modeling and provability of two types of CRDT’s as outlined in the Shapiro et. al. work in A Comprehensive Study of Convergent and Commutative Replicated Data Types. The video is finally available online and the source code is available on GitHub. The repo also contains some basic modeling of some of Conway’s work outlined in Logic and Lattices for Distributed Programming. The slides are also available.
We’ll briefly look at the grow-only counter, which is very similar to a vector clock. Since understanding the clock data structure is required to begin proving facts about vectors of them, let’s dig into clocks first.
Let’s first define a map of clocks as a finite map of natural numbers.
Let’s define two functions for working with clocks. Remember, that functions need to be totally ordered to ensure termination. The find function for working with maps is going to return an option nat, so we author our pattern matches accordingly.
Now, we can begin proving certain properties about clocks. First, we
can prove that merge is commutative because the
max operation is
commutative over natural numbers. We simply destructure the clock
functions, simplify the terms and apply the existing lemma.
In the same way, we can prove that the merging of two clocks are idempotent and associative for similar reasons; both hold true beacuse the max operation is both associative and idempotent.
Finally, we can define a proof which will help us later on that shows that comparing a clock to itself always returns true (specifically because less than or equal to is a partial ordering over natural numbers). This will help us later when attempting to prove certain properties about G-Counters monotonically advancing.
G-Counter represents a grow-only counter, and is modeled similarly
to a vector clock. A series of actor/increment pairs are stored in a
vector, and the sum of the counter is derived by a
fold across the
First, let’s define a
G-Counter as a
ClockMap, as defind above, with
the values of the map also as natural numbers. Then, we define a
function to initialize an empty
Then, let’s define a function for incrementing a particular actor in a map of clocks. This is simply done by pattern matching the find, and calling the successor function on the existing actor’s value if it’s present.
Then, we define a function to reveal the current value of the counter by
fold over the values and perfoming a sum.
To merge, we can just use
map2 with our existing merge function.
To test equality, we can use the built-in equality test for maps.
Finally, to compare, we can apply the comparison function to the two maps of clocks, and then test equality against a map of true values of the same length, which will allow us to test of one map is a partial ordering of another map.
So, now we can begin proving aspects about
First, let’s prove that merge is commutative.
Given that we’ve already proven that merging two clocks is commutative,
we simply need to destructure the
G-Counter to a point where we can
apply the previously defined lemma.
Similarly, we can also prove that the merge operation is idempotent and associative, as we’ve already proven properties about these operations over clocks.
Next, we can prove that the increment function monotonically advances the data structure by using our comparison function between an pre- and post-incremented data structure.
This proof gets a little bit more complex, having to prove facts about incrementing a value when its present vs. not present in an existing map of clocks. However, again, using the facts we’ve already proven over clocks, we can simply apply our existing lemmas.
Finally, we can prove that the merge operation monotonically advances the data structure, by again comparing the pre- and post-merged data structures. Since our comparison function operates over natual numbers, using the less than or equal to operator, we can simply destructure the merge operation, and apply a lemma showing that max and less than or equal to, preserve partial ordering.
There you have it.
I haven’t been able to finish a proper proof of partial ordering
G-Counters yet, but I’m currently actively working on
it. I hope to address both that, and
PN-Counters in a subsequent blog
Feedback is encouraged!
Updated 2013-06-11: Added link to slides.
View this story on Hacker News.