Christopher Meiklejohn

home lasp research courses publications videos code curriculum vitae

Verified Vector Clocks: An Experience Report, Part 2

19 Nov 2013

This post outlines a bunch of experimental work I’ve completed to model data structures in Coq, leveraging Tim Carstens’ verlang project to extract the data structures into executable Erlang.

Here’s a link to the first post in this series.

Updated March 8th, 2014: A full talk about this work was presented at Erlang Factory, San Francisco 2014. Both the slides and video are available.

Extending with timestamps

Let us extend our existing model to carry timestamps, as the riak_core model does. In core, we model the actual item in the vector clock as nested tuples structured similar to the following:

These timestamps are generated with Erlang code, which is similar to the following, but optimized:

This produces a monotonically advancing integer representing the current time in seconds. Note, this time is system dependent, succeptable to clock skew and all of the other wonderful things that come with using wall clock time. That aside, we are aiming to model something that could be used as a replacement for the existing Riak Core vclock model, so we will go with this model.

We will start by modifying our types to model the timestamp as a natural number, and abstract the functions used to initialize and increment it so we can replace these with the actual calls to the timestamp generating function in Erlang.

We will begin by modeling the clock itself as product of products, essentially a triple as a product is formed like the following:

See the implementation below:

Let us now add some functions for handling the incrementing and initializing of values:

Let us now update our functions to increment the timestamp accordingly:

Finally, let us add a function to return the timestamps:

Now, to figure out how to implement the prune functionality, starting by examining the implementation of prune in Riak Core.

For more information on why we have to prune, check out the classic “Why Vector Clocks Are Hard” article from the Basho blog.

The first thing we see is that we do not prune the vector clock if it is still considered small.

In the case where the vector clock is no longer considered small, we take the earliest clock, from the lexographically earliest actor, and attempt to determine if it is still considered young. If it is, we do nothing. If not, our vector clock has candidates for pruning.

Let’s examine the next function call. In the false case, unless the vector clock is considered large, or the timestamp is considered old, we do not perform the prune.

Then we repeat the entire process with the tail of the list, given that the head was prime for pruning.

Now, we’ve run into a couple problems:

• We have no way to access properties stored in buckets, or the application environment in Riak.
• We have no easy way to work with the pure Erlang structures in Coq.

So, the approach we will take is implementing a prune function in Coq, which will take all of the environmental arguments explicitly, and then we will write a function in our Erlang module to bridge the gap between the data structures in Coq and in Erlang.

Here’s what our prune function looks like in Coq.

In the next post, we’ll look at how we begin integrating this with the vclock module in Riak Core.