Verified Vector Clocks: An Unexpected Journey

In a distributed system, where data structures are replicated or shared between multiple communicating nodes, it is highly desirable to have a method for asserting that certain invariants are preserved after objects are manipulated. In industry, one of the major approaches is using property-based testing utilities such as QuickCheck to verify that certain properties hold true over multiple inter-leavings of operations applied to these data structures. However, given the amount of possible executions as the number of nodes or processes grow, exhausting that state space becomes more difficult. An alternative approach for this type of verification is to use an interactive theorem prover, which we discuss below.
We explore vvclocks, a new Erlang library which provides a formally verified implementation of vector clocks for use in Erlang applications. We describe the process of building a this implementation, as outlined by Lamport in 1978, in the Coq proof assistant and walk through the process of using Coq’s code extraction utilities to generate Core Erlang code. To verify the applicability of this implementation, we replace the vector clock implementation in the open source Dynamo-based data store, Riak. We explore the process of writing an adapter to translate between the Coq-derived data structures and the base Erlang data structures, adapting the existing test suite to pass, as well as running the Riak data store with the newly verified implementation of vector clocks.

Talk objectives:

Explore alternative ways of testing Erlang code, provide an introduction to the formal verification system Coq, as well as teach the fundamentals of Core Erlang.

Target audience:

Erlang and distributed systems engineers who look to formally verify their applications to ensure proper operation.

Slides
Video

About Christopher

Christopher Meiklejohn loves distributed systems and programming languages. Previously, Christopher worked at Basho Technologies, Inc. on the distributed key-value store, Riak. Christopher develops a programming language for distributed computation, called Lasp. Christopher is currently a Ph.D. student at the Université Catholique de Louvain in Belgium.

GitHub: cmeiklejohn

Twitter: @cmeik

Back to conference page