Linearizability is a well-established correctness criterion for concurrent data types and it corresponds to one of the three desirable properties of a distributed system, namely consistency. The intuition behind linearizability is that all operations in a so-called history can be reordered along a timeline such that a given sequential specification holds. Given a history and sequential specification, a linearizability checker checks whether such a reordering exists.
In general, checking linearizability is NP-complete and so writing an efficient linearizability checker is inherently difficult. This is motivation to experimentally compare various techniques to find out what works well in practice - the purpose of this source code repository.
For our experiments, we collected histories from Intel's Threading Building Blocks (TBB) library, Siemens's Embedded Multicore Building Blocks (EMBB) library, and the distributed key-value store etcd using Jepsen.
In a nutshell, the result of our work is a linearizability checker that can check CP distributed systems on which current implementations timeout or run out of memory.
Consider the following history H of read and write operations on a register:
write(1) read() : 2
|----------| |------------|
write(2)
|----------|
The write(1) happens-before the two remaining read() and write(2) operations.
Note that read() and write(2) happen concurrently because neither finishes before
the other starts. Then H is linearizable because the operations can be reordered as
follows:
write(1); write(2); read()
where the read returns the last written register value, namely 2. By contrast, the
following history H' is non-linearizable because there is no valid reordering of
reads and writes that satisfies the expected behaviour of a register:
write(1) read() : 2
|----------| |------------|
write(2)
|----------|
A detailed discussion of related work is given in our FORTE'15 paper. Here, we only mention that there has been surprisingly little work done in systematically evaluating and comparing possible linearizability algorithms, the various ways they can be implemented, or trying out ideas from the SAT solver community.
We published the most relevant experimental results in FORTE'15. Under the assumption of so-called P-compositionality, we show that our technique improves Lowe's state-of-the-art linearizability checker by one order of magnitude, in space and/or time.
This repository gives the source code that is required for all the experiments, including additional ones that we did not discuss in the paper due to space. To compile our source code, a C++11-compliant compiler is required.
To repeat our experiments with Lowe's concurrent set implementations, run the following command:
$ make hashset-test
In addition, by downloading, compiling and configuring TBB and EMBB in the Makefile, you will also be able to run the other experiments.
You may be also interested in running experiments with etcd 2.0 which we did not have space to discuss in the paper:
$ make etcd-test
This runs our tool against 100 collected etcd histories, and completes in a few
seconds. By contrast, Knossos times out on benchmark 7 and 99, and
runs out of memory on 40, 57, 85 and 97 (all benchmarks can be found in the
jepsen directory). Note that the failures in etcd are
expected here because we allow read requests to bypass the consensus protocol
(by setting quorum=false)! As a sanity check, we have also tried three tests
with quorum=true and we did not find any linearizability bugs.
We have implemented a new linearizability checker that we evaluated through extensive experiments on TBB, EMBB and etcd. We found that our linearizability checker can solve instances on which current implementations timeout or run out of memory.
Of course, there are always things to improve, and we warmly invite any form of feedback, questions etc. We also welcome patches (including benchmarks) as Github pull requests.