synchronous-tla-benchmarks
Several synchronous fault-tolerant distributed algorithms encoded in TLA+. These benchmarks were checked using the model checker TLC in the following paper:
Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, Florian Zuleger.
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction.
VMCAI 2018
This repository contains the following benchmarks:
| Name | Problem | Reference |
|---|---|---|
| edac | early deciding consensus | Charron-Bost, Schiper |
| fair_cons | consensus | Raynal, p.17 |
| floodmin_k1 | k-set agreement, for k=1 | Lynch, p.136 |
| floodmin_k2 | k-set agreement, for k=2 | Lynch, p.136 |
| floodset | consensus | Lynch, p.103 |
| nbac | non-blocking atomic commit | Raynal, p.82 |
| pdif | early stopping consensus | Raynal, p.38 |
All of the benchmarks assume the crash fault model, where at most T of the total N processes in the system can fail by crashing, with T < N. Once a process crashes, it stops executing the algorithm and it cannot restart.
For each benchmark name, the directory name contains the following TLA+ files:
name.tla- this is a concrete encoding of the algorithm, that can be used to check the safety and liveness properties of the algorithm for small system instances, e.g., up to N = 5 processes. When checking, one needs to assign concrete values to the parameters N, T, F.name_abstract.tla- this is an abstract encoding of the algorithm, that can be used to check the safety and liveness properties in the parameterized case, that is, for all values of the parameters N, T, F. In this encoding, the behavior of a small number M of processes (usually 2 or 3) is kept as in the concrete system, while the behavior of the remaining N - M processes is abstracted. The M processes are assumed to be correct, which implies that T <= N - M.name_abstract_m'.tla- this is an abstract encoding that captures the corner cases where M' < M processes are fixed and assumed correct, that is, when N - M < T < N.
For more details, and for our experimental results, please check the VMCAI 2018 paper.