Skip to content

Synchronous fault-tolerant distributed algorithms encoded in TLA+

License

Notifications You must be signed in to change notification settings

istoilkovska/synchronous-tla-benchmarks

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

9 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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.

About

Synchronous fault-tolerant distributed algorithms encoded in TLA+

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages