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.