An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Coq Python OCaml Shell Ruby Makefile Other
Clone or download
Permalink
Failed to load latest commit information.
.travis correct rsa keys Jan 22, 2018
config deployment fixes Apr 25, 2018
extraction switch to strings for client ids and generate UUIDs in clients Dec 17, 2017
lib/capistrano/tasks experiments comparing vard with vard-serialized-log Jul 5, 2018
proofalytics update proofalytics scripts to Xenial Travis environment Jan 23, 2018
raft-proofs deployment fixes Apr 25, 2018
raft client id type specified in Raft parameters Dec 17, 2017
script updated coqproject.sh Dec 2, 2017
systems switch to strings for client ids and generate UUIDs in clients Dec 17, 2017
vagrant Improve vard to use CompCert's PTree for store key-value state. Nov 7, 2015
.gitignore deployment fixes Apr 25, 2018
.hook.yaml introduce build.sh, add support for hooknook builds Feb 21, 2015
.travis-ci.sh Travis script formatting, use 32bit Coq 8.7 Jan 6, 2018
.travis.yml Coq 8.8 officially supported Apr 27, 2018
Capfile Capistrano-based deployment (#59) Jul 26, 2017
LICENSE Verdi is licensed under the BSD 2-clause license Apr 17, 2015
Makefile deployment fixes Apr 25, 2018
Makefile.detect-coq-version adapt Coq version detection from mathcomp; 8.6, 8.7 and trunk/master … Jul 24, 2017
PROOF_ENGINEERING.md Public Verdi release Feb 10, 2015
README.md Coq 8.8 officially supported Apr 27, 2018
STYLE.md fix and clarify documentation May 21, 2017
Vagrantfile Add Vagrant configuration and vim setup Oct 13, 2015
build.sh update disco repos for Travis, build.sh params, fix README Nov 21, 2016
configure Raft with both serialized message and log transformer (given IOStream… Sep 11, 2017
vard-log.opam deployment fixes Apr 25, 2018
vard-serialized-log.opam deployment fixes Apr 25, 2018
vard-serialized.opam deployment fixes Apr 25, 2018
vard.opam deployment fixes Apr 25, 2018
verdi-raft-checkproofs.opam deployment fixes Apr 25, 2018
verdi-raft.descr switch to safe_string for vard, use arr_of_string from Util May 26, 2017
verdi-raft.opam deployment fixes Apr 25, 2018
words10.txt experiments comparing vard with vard-serialized-log Jul 5, 2018
words50.txt experiments comparing vard with vard-serialized-log Jul 5, 2018

README.md

Verdi Raft

Build Status

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework.

Requirements

Definitions and proofs:

Executable vard key-value store:

Client for vard:

Integration testing of vard:

Unit testing of unverified vard code:

Building

We recommend installing the dependencies of Verdi Raft via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add distributedcomponents-dev http://opam-dev.distributedcomponents.net
opam install verdi StructTact verdi-runtime ocamlbuild cheerios cheerios-runtime

Then, run ./configure in the Verdi Raft root directory. This will check for the appropriate version of Coq and ensure all necessary Coq dependencies can be located. By default, Verdi, StructTact, and Cheerios are assumed to be installed in Coq's user-contrib directory, but this can be overridden by setting the Verdi_PATH, StructTact_PATH, and Cheerios_PATH environment variables.

Finally, run make in the root directory. This will compile the Raft implementation and proof interfaces, and check all the proofs. To speed up proof checking on multi-core machines, use make -jX, where X is at least the number of cores.

To build the vard key-value store program in extraction/vard, run make vard in the root directory. If the implementation has been compiled as above, this simply compiles the extracted OCaml code to a native program; otherwise, the implementation is extracted to OCaml and compiled without checking any proofs.

Files

The raft and raft-proofs subdirectories contain the implementation and verification of Raft. For each proof interface file in raft, there is a corresponding proof file in raft-proofs. The files in the raft subdirectory include:

  • Raft.v: an implementation of Raft in Verdi
  • RaftRefinementInterface.v: an application of the ghost-variable transformer to Raft which tracks several ghost variables used in the verification of Raft
  • CommonTheorems.v: several useful theorems about functions used by the Raft implementation
  • OneLeaderPerTermInterface: a statement of Raft's election safety property. See also the corresponding proof file in raft-proofs.
    • CandidatesVoteForSelvesInterface.v, VotesCorrectInterface.v, and CroniesCorrectInterface.v: statements of properties used by the proof OneLeaderPerTermProof.v
  • LogMatchingInterface.v: a statement of Raft's log matching property. See also LogMatchingProof.v in raft-proofs
    • LeaderSublogInterface.v, SortedInterface.v, and UniqueIndicesInterface.v: statements of properties used by LogMatchingProof.v

The file EndToEndLinearizability.v in raft-proofs uses the proofs of all proof interfaces to show Raft's linearizability property.

The vard Key-Value Store

vard is a simple key-value store implemented using Verdi. vard is specified and verified against Verdi's state-machine semantics in the VarD.v example system distributed with Verdi. When the Raft transformer is applied, vard can be run as a strongly-consistent, fault-tolerant key-value store along the lines of etcd.

After running make vard in the root directory, OCaml code for vard is extracted, compiled, and linked against a Verdi shim and some vard-specific serialization/debugging code, to produce a vard.native binary in extraction/vard.

Running make bench-vard in extraction/vard will produce some benchmark numbers, which are largely meaningless on localhost (multiple processes writing and fsync-ing to the same disk and communicating over loopback doesn't accurately model real-world use cases). Running make debug will get you a tmux session where you can play around with a vard cluster in debug mode; look in bench/vard.py for a simple Python vard client.

As the name suggests, vard is designed to be comparable to the etcd key-value store (although it currently supports many fewer features). To that end, we include a very simple etcd "client" which can be used for benchmarking. Running make bench-etcd will run the vard benchmarks against etcd (although see above for why these results are not particularly meaningful). See below for instructions to run both stores on a cluster in order to get a more useful performance comparison.

Running vard on a cluster

vard accepts the following command-line options:

-me NAME             name for this node
-port PORT           port for client commands
-dbpath DIRECTORY    directory for storing database files
-node NAME,IP:PORT   node in the cluster
-debug               run in debug mode

Note that vard node names are integers starting from 0.

For example, to run vard on a cluster with IP addresses 192.168.0.1, 192.168.0.2, 192.168.0.3, client (input) port 8000, and port 9000 for inter-node communication, use the following:

# on 192.168.0.1
$ ./vard.native -dbpath /tmp/vard-8000 -port 8000 -me 0 -node 0,192.168.0.1:9000 \
                -node 1,192.168.0.2:9000 -node 2,192.168.0.3:9000

# on 192.168.0.2
$ ./vard.native -dbpath /tmp/vard-8000 -port 8000 -me 1 -node 0,192.168.0.1:9000 \
                -node 1,192.168.0.2:9000 -node 2,192.168.0.3:9000

# on 192.168.0.3
$ ./vard.native -dbpath /tmp/vard-8000 -port 8000 -me 2 -node 0,192.168.0.1:9000 \
                    -node 1,192.168.0.2:9000 -node 2,192.168.0.3:9000

When the cluster is set up, a benchmark can be run as follows:

# on the client machine
$ python2 bench/setup.py --service vard --keys 50 \
                         --cluster "192.168.0.1:8000,192.168.0.2:8000,192.168.0.3:8000"
$ python2 bench/bench.py --service vard --keys 50 \
                         --cluster "192.168.0.1:8000,192.168.0.2:8000,192.168.0.3:8000" \
                         --threads 8 --requests 100

Running etcd on a cluster

We can compare numbers for vard and etcd running on the same cluster as follows:

# on 192.168.0.1
$ etcd --name=one \
 --listen-client-urls http://192.168.0.1:8000 \
 --advertise-client-urls http://192.168.0.1:8000 \
 --initial-advertise-peer-urls http://192.168.0.1:9000 \
 --listen-peer-urls http://192.168.0.1:9000 \
 --data-dir=/tmp/etcd \
 --initial-cluster "one=http://192.168.0.1:9000,two=http://192.168.0.2:9000,three=http://192.168.0.3:9000"

# on 192.168.0.2
$ etcd --name=two \
 --listen-client-urls http://192.168.0.2:8000 \
 --advertise-client-urls http://192.168.0.2:8000 \
 --initial-advertise-peer-urls http://192.168.0.2:9000 \
 --listen-peer-urls http://192.168.0.2:9000 \
 --data-dir=/tmp/etcd \
 --initial-cluster "one=http://192.168.0.1:9000,two=http://192.168.0.2:9000,three=http://192.168.0.3:9000"

# on 192.168.0.3
$ etcd --name=three \
 --listen-client-urls http://192.168.0.3:8000 \
 --advertise-client-urls http://192.168.0.3:8000 \
 --initial-advertise-peer-urls http://192.168.0.3:9000 \
 --listen-peer-urls http://192.168.0.3:9000 \
 --data-dir=/tmp/etcd \
 --initial-cluster "one=http://192.168.0.1:9000,two=http://192.168.0.2:9000,three=http://192.168.0.3:9000"

# on the client machine
$ python2 bench/setup.py --service etcd --keys 50 \
                         --cluster "192.168.0.1:8000,192.168.0.2:8000,192.168.0.3:8000"
$ python2 bench/bench.py --service etcd --keys 50 \
                         --cluster "192.168.0.1:8000,192.168.0.2:8000,192.168.0.3:8000" \
                         --threads 8 --requests 100