Verified Vector Clocks: An Experience Report, Part 1
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.
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.
Modeling vector clocks
Let us start by modeling vector clocks in Coq. We will start by
focusing on the API exposed by riak_core’s vector clock
implementation.
For this first implementation, we’re going to implement the API without the timestamps that vclock uses for pruning for a couple reasons: they are not core to an implementation of vector clocks or version vectors, and there does not appear to be a good way to model UNIX timestamps in Coq.
First, some boilerplate and type definitions. We’ll be modeling the
vclock as a list of pairs, each pair representing a particular actor
and the count of events observed. In the actual Riak implementation,
this is modeled as the product of atoms and integers.
Keep in mind these are not the most efficient implementations of these methods, we are mainly focusing on naive implementations where we can easily debug the translation to Core Erlang incase it fails.
Require Import Coq.Lists.List.
Require Import Coq.Arith.EqNat.
Require Import Coq.Bool.Bool.
Module VVClock.
Definition actor := nat.
Definition count := nat.
Definition clock := (actor * count)%type.
Definition vclock := list clock%type.Now, let’s add our constructor functions:
Definition fresh : vclock := nil.Now, our functions to increment an actor.
(** Return a single arity function which searches for a particular
actor. *)
Definition find' (actor : actor) :=
fun clock : clock => match clock with
| pair x _ => beq_nat actor x
end.
(** Return a single arity function which will be filter predicate for
actor. *)
Definition find'' (actor : actor) :=
fun clock : clock => match clock with
| pair x _ => negb (beq_nat actor x)
end.
(** Increment actor in the vclock *)
Definition increment (actor : actor) (vclock : vclock) :=
match find (find' actor) vclock with
| None =>
cons (pair actor 1) vclock
| Some (pair x y) =>
cons (pair x (S y)) (filter (find' actor) vclock)
end.
*)Some functions to compare equality amongst vector clocks:
Definition equal' status_and_vclock (clock : clock) :=
match clock, status_and_vclock with
| pair actor count,
pair status vclock => match find (find' actor) vclock with
| None =>
pair false vclock
| Some (pair _ y) =>
pair (andb
status
(beq_nat count y)) vclock
end
end.
Definition equal (vc1 vc2 : vclock) :=
match fold_left equal' vc1 (pair true vc2) with
| pair false _ =>
false
| pair true _ =>
match fold_left equal' vc2 (pair true vc1) with
| pair false _ =>
false
| pair true _ =>
true
end
end.Some functions to compare vector clocks and ensure a proper partial ordering:
Fixpoint ble_nat (n m : nat) {struct n} : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => ble_nat n' m'
end
end.
Definition descends' status_and_vclock (clock : clock) :=
match clock, status_and_vclock with
| pair actor count,
pair status vclock => match find (find' actor) vclock with
| None =>
pair false vclock
| Some (pair _ y) =>
pair (andb
status
(ble_nat count y)) vclock
end
end.
Definition descends (vc1 vc2 : vclock) :=
match fold_left descends' vc2 (pair true vc1) with
| pair false _ =>
false
| pair true _ =>
true
end.And, finally some functions to perform the merge betwen two vector clocks.
Definition max' (vclock : vclock) (clock : clock) :=
match clock with
| pair actor count => match find (find' actor) vclock with
| None =>
cons (pair actor count) vclock
| Some (pair _ y) =>
cons (pair actor (max count y))
(filter (find'' actor) vclock)
end
end.
Definition merge (vc1 vc2 : vclock) := fold_left max' vc1 vc2.Qed, one might say.
Examining the extracted code
Extraction Language CoreErlang.
Recursive Extraction VVClock.Let us now examine the generated code.
One of the first problems that we encounter is that the function used to construct the vector clock is not extracted. Let’s manually create this function in the extracted Core Erlang.
'fresh'/0 = fun () ->
[]We also modify the module exports at the top to reflect this as well.
Next, we’ll notice that there are a bunch of function calls which are
incorrectly qualified as calls to vvclock.VVClock, which we’ll
manually modify to contain the correct call. These are calls to
functions within the vvclock module.
call 'vvclock':'ble_nat'
( _actor
, _a
)Another problem we run into are function calls which have not been fully
qualified with their arity. For example, the call to descends@ missing
its arity, descends@/2.
'descends'/2 = fun (_vc1, _vc2) ->
case call 'Coq.Lists.List':'fold_left'
( 'descends@'
, _vc2
, { 'Pair'
, 'True'
, _vc1
}
) Finally, we run into a problem with currying, where function calls like the following…
Definition find'' (actor : actor) :=
fun clock : clock => match clock with
| pair x _ => negb (beq_nat actor x)
end.…get exported to something like the following:
'find@'/2 = fun (_actor, _clock) ->
case _clock of
{ 'Pair'
, _c
, _x
} when 'true' ->
call 'Coq.Arith.EqNat':'beq_nat'
( _actor
, _c
)
end…which causes code like the following, to fail:
case call 'Coq.Lists.List':'find'
( call 'vvclock':'find@' (_actor)
, _vclock
) ofIn cases like this, we have solved the problem by manually inlining the call to the find function.
Now, given that we have modeled these clocks as products of Peano
numbers, we can take the existing riak_core test suite, and execute
it with only a slight modification and watch the tests pass.
riak_core_test() ->
A = vvclock:fresh(),
B = vvclock:fresh(),
A1 = vvclock:increment('O', A),
B1 = vvclock:increment({'S', 'O'}, B),
B2 = vvclock:increment({'S', 'O'}, B1),
io:format("A: ~p~n", [A]),
io:format("B: ~p~n", [B]),
io:format("A1: ~p~n", [A1]),
io:format("B1: ~p~n", [B1]),
io:format("B2: ~p~n", [B2]),
'True' = vvclock:descends(A1, A),
'True' = vvclock:descends(B1, B),
'False' = vvclock:descends(A1, B1),
A2 = vvclock:increment('O', A1),
C = vvclock:merge(A2, B1),
C1 = vvclock:increment({'S', {'S', 'O'}}, C),
io:format("A2: ~p~n", [A2]),
io:format("C: ~p~n", [C]),
io:format("C1: ~p~n", [C1]),
'True' = vvclock:descends(C1, A2),
'True' = vvclock:descends(C1, B1),
'False' = vvclock:descends(B1, C1),
'False' = vvclock:descends(B1, A1),
ok.And, for those of you interested in the output:
A: []
B: []
A1: [{'Pair','O',{'S','O'}}]
B1: [{'Pair',{'S','O'},{'S','O'}}]
B2: [{'Pair',{'S','O'},{'S',{'S','O'}}}]
A2: [{'Pair','O',{'S',{'S','O'}}}]
C: [{'Pair','O',{'S',{'S','O'}}},{'Pair',{'S','O'},{'S','O'}}]
C1: [{'Pair',{'S',{'S','O'}},{'S','O'}},
{'Pair','O',{'S',{'S','O'}}},
{'Pair',{'S','O'},{'S','O'}}]Cool, that’s not a bad start. We can’t directly apply this to Riak yet, as the true and false atoms are represented as constructors for the Boolean type in Coq, and we’re stuck using Peano numbers. We also don’t have any proofs yet of these functions.
We will be addressing both of these issues, as well as how we adapted this library for use in the Riak data store in subsequent posts.
This code is available on GitHub as an OTP application and video and slides are available of a lightning talk I did on this work at RICON|West 2013.
Christopher S. Meiklejohn is a Software Engineering Ph.D. candidate in the Software and Societal Systems Department at the School of Computer Science of Carnegie Mellon University.
[email protected]
[email protected]
filibuster.cloud