Updated March 8th, 2014: A full talk about this work was presented at Erlang
Factory, San Francisco 2014. Both the
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
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.
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.