pviotti / conver-old

[discontinued, see pviotti/conver] Practical verification of non-transactional consistency models.

Con:heavy_check_mark:er

Conver verifies implementations of the most common non-transactional consistency models.
It spawns client processes that perform concurrent reads and writes on the distributed store, and records their outcomes. After the execution, it builds graph entities that express ordering and mutual visibility of operations. Finally, it uses such graph entities to check consistency semantics defined as first-order logic predicates.

The approach implemented in Conver has been described in this PaPoC 2016 paper.

NOTE: this project is currently unmaintained. I decided to rewrite it in Scala for practical convenience. The Scala version features a linearizability checker (which this project lacks), and improved consistency checks.

Features

Datastores currently supported: ZooKeeper and Riak.

Currently, Conver can verify the following consistency semantics: Monotonic Reads, Monotonic Writes, Read-your-writes, PRAM, Writes-follow-reads, Causal and Strong Consistency (regularity).
To have an overview of the consistency models verified by Conver, see this survey.

Besides textual output, Conver generates a visualization of the executions, highlighting the violations of consistency models.

Getting started

Once installed Erlang/OTP (R18+), to build Conver issue:

$ make

The dstores folder contains scripts to build and locally run Docker clusters of different storage systems.
For instance, to build and run a cluster of ZooKeeper servers issue make build-zk and make start-zk.
To query the cluster status use make status-zk, and to stop it make stop-zk.
Additionally, the script dstores/net.sh offers functions to simulate slow and lossy networks.

Once the storage system is running and its configuration parameters are recorded in conver.conf, to run a Conver test issue:

$ ./conver run <num> <mock|zk|riak>

where num is the number of client processes (e.g., 3), followed by a string that identifies the store under test (mock for a dummy in-memory store consisting of Erlang's ets, zk for ZooKeeper, riak for Riak).

For comparison, you can run a traditional property-based test suite on the dummy in-memory database using PropEr by issuing ./conver proper.

Similar projects: Jepsen, Hermitage.

Authors and license

Conver has been developed at EURECOM.
License: Apache 2.0.

conver-old's Issues

Package as Docker run script

Fix process naming

Processes can't be more than the letter of the alphabet. Find a more scalable way to name processes.

Fix monotonicity checks of reads and writes

The code that checks monotonicity of read and write of a given session is convoluted and probably buggy.

Add tests based on exemplary incorrect executions

(this has been implemented in the Scala version of Conver)

Implement linearizability checker

Implement a graph-based linearizability checker.
(this has been implemented in the Scala version of Conver)