• Stars
    star
    178
  • Rank 210,036 (Top 5 %)
  • Language Coq
  • License
    BSD 2-Clause "Sim...
  • Created over 7 years ago
  • Updated 6 months ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

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

Verdi Raft

Docker CI

Raft is a distributed consensus algorithm that is designed to be easy to understand and is equivalent to Paxos in fault tolerance and performance. Verdi Raft is a verified implementation of Raft in Coq, constructed using the Verdi framework. Included is a verified fault-tolerant key-value store using Raft.

Meta

Optional requirements

Executable vard key-value store:

Client for vard:

Integration testing of vard:

Unit testing of unverified vard code:

Building and installation instructions

We recommend installing the dependencies of Verdi Raft via opam:

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install coq-struct-tact coq-cheerios coq-verdi

Then, 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 on your machine.

To build the vard key-value store program in extraction/vard, you first need to install its requirements. Then, run make vard in the root directory. If the Coq implementation has been compiled as above, this simply compiles the extracted OCaml code to a native executable; 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

More Repositories

1

verdi

A framework for formally verifying distributed systems implementations in Coq
Coq
575
star
2

tensat

Re-implementation of the TASO compiler using equality saturation
Rust
108
star
3

ruler

Rewrite Rule Inference Using Equality Saturation
Rust
105
star
4

Cassius

A CSS specification and reasoning engine
Racket
90
star
5

herbgrind

A Valgrind tool for Herbie
C
90
star
6

crust

A compiler from Rust to C, and a checker for unsafe code
Rust
81
star
7

PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
OCaml
50
star
8

Casper

A compiler for automatically re-targeting sequential Java code to Apache Spark.
Java
49
star
9

pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
Coq
49
star
10

szalinski

Szalinski: A Tool for Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
OpenSCAD
41
star
11

CoqAST

Fun plugin to play with the Gallina AST.
OCaml
37
star
12

oddity

A graphical, time-traveling debugger for distributed systems
Clojure
32
star
13

cheerios

Formally verified Coq serialization library with support for extraction to OCaml
Coq
23
star
14

dexter

a compiler for re-writing image processing functions in C++ to Halide
Java
22
star
15

synapse

Optimizing Synthesis with Metasketches, POPL 2016
Racket
22
star
16

StructTact

Coq utility and tactic library.
Coq
21
star
17

memsynth

An advanced automated reasoning tool for memory consistency model specifications.
Alloy
19
star
18

rake

compiling DSLs to high-level hardware instructions
Racket
19
star
19

stng

compiler for fortran stencils using verified lifting,
C++
17
star
20

oeuf

gallina frontend for CompCert
Coq
17
star
21

ferrite

Ferrite, a toolkit for developing file system crash-consistency models
Racket
16
star
22

potpie

Proof Object Transformation, Preserving Imp Embeddings: the first proof compiler to be formally proven correct
Coq
13
star
23

reincarnate-aec

Reincarnate Artifact for ICFP 2018
JavaScript
13
star
24

magic

Demystifying the magic of supertactics
OCaml
13
star
25

arvo

A proof assistant.
C
12
star
26

coq-plugin-lib

Library of useful utility functions for Coq plugins
OCaml
11
star
27

SaltShaker

Verifying x86 semantics
Shell
10
star
28

concerto

Combined concrete and abstract interpretation
Java
7
star
29

crimp

Certified Relational to Imperative
Coq
5
star
30

analytics-data

Coq
5
star
31

incarnate-exploration-archive

PL for 3D Printing
OpenSCAD
5
star
32

peek

Peek: a verified peephole optimizer for CompCert
Coq
5
star
33

iag-synthesis

Parallel, incremental evaluation of attribute grammars through synthesis
HTML
4
star
34

bagpipe

Reasoning about BGP configurations. Public development repo.
Coq
4
star
35

theia

Automatically Visualizing Program Execution
OCaml
4
star
36

fix-to-elim

Fixpoint to eliminator translation in Coq
Coq
3
star
37

coq-change-analytics

REPLICA: REPL Instrumentation for Coq Analysis
Python
3
star
38

scout

Using High-Level Design Constraints to Automatically Generate Design Alternatives
Jupyter Notebook
3
star
39

syncro

Synthesis of Incremental Operations
Racket
2
star
40

legato

Legato is a static analysis for finding bugs in dynamic resource usage
Java
2
star
41

univalent-rewrites

POPL 2020 PUMPKIN/DEVOID submission
TeX
2
star
42

staccato

Stale Configuration and Consistency Analysis Tool
Java
2
star
43

pumpkin

Public webpage for Pumpkin Patch
HTML
1
star
44

VeriCQ

Use SpaceSearch to verify Conjunctive Query Rewrite Rules
Perl
1
star
45

epics-tools

Static analysis tools for EPICS
Haskell
1
star
46

PUMPKIN-git

A prototype PUMPKIN PATCH interface with Git integration
OCaml
1
star
47

seguard-resources

SeGuard Public Resources
HTML
1
star
48

nightly-conf

The public nightly server configuration
1
star
49

majortom

An Oddity shim for "arbitrary" x86-64 Linux binaries
Rust
1
star