Skip to content

Latest commit

 

History

History
82 lines (72 loc) · 14.1 KB

README.md

File metadata and controls

82 lines (72 loc) · 14.1 KB
Raw

Welcome to TLA+ Benchmarks

The page TLA+ Benchmarks is a library of TLA+ specifications for distributed algorithms. The webpage supplies the TLA+ community with:

  • A comprehensive library of the TLA+ specifications that are available today, in order to provide an overview of how to specify an algorithm in TLA+.
  • A comprehensive list of references and other interesting information for each problem.

Do you have your own case study that you like to share with the community? Send a pointer to us and we will include it in the repository. Your specifications will help the community in improving the tools for TLA+ analysis.

List of benchmarks

No Name Short description Spec's authors TLAPS Proof TLC Check Used modules
1 2PCwithBTM A modified version of P2TCommit (Gray & Lamport, 2006) Murat Demirbas ✔ FinSet, Int, Seq
2 802.16 IEEE 802.16 WiMAX Protocols Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou ✔ Int, Seq, FinSet
3 aba-asyn-byz Asynchronous Byzantine agreement (Bracha & Toueg, 1985) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Nat
4 acp-nb Non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) Stephan Merz ✔ default theories
5 acp-nb-wrong Wrong version of the non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) Stephan Merz ✔ default theories
6 acp-sb Non-blocking atomic commitment with a simple broadcast (Babaoğlu & Toueg, 1993) Stephan Merz ✔ default theories
7 allocator Specification of a resource allocator Stephan Merz ✔ FinSet
8 async-comm The diversity of asynchronous communication (Chevrou et al., 2016) Florent Chevrou, Aurélie Hurault, Philippe Quéinnec ✔ Nat
9 bcastByz Asynchronous reliable broadcast - Figure 7 (Srikanth & Toeug, 1987) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ ✔ Nat, FinSet
10 bcastFolklore Folklore reliable broadcast - Figure 4 (Chandra and Toueg, 1996) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ ✔ Nat
11 bosco One-Step Byzantine asynchronous consensus (Song & Renesse, 2008) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Nat, FinSet
12 Boulangerie A variant of the bakery algorithm (Yoram & Patkin, 2015) Stephan Merz ✔ ✔ Int
13 byihive Based on RFC3506 - Requirements and Design for Voucher Trading System (Fujimura & Eastlake) Santhosh Raju ✔ default theories
14 byzpaxos Byzantizing Paxos by Refinement (Lamport, 2011) Leslie Lamport? ✔ Int, FinSet
15 c1cs Consensus in one communication step (Brasileiro et al., 2001) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Int, FinSet
16 Caesar Multi-leader generalized consensus protocol (Arun et al., 2017) Giuliano Losa ✔ FinSet, Seq, Int
17 CarTalkPuzzle A TLA+ specification of the solution to a nice puzzle. ✔ Int
18 CASPaxos An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov) Tobias Schottdorf ✔ Int, FinSet
19 cbc_max Condition-based consensus (Mostefaoui et al., 2003) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Int, FinSet
20 cf1s-folklore One-step consensus with zero-degradation (Dobre & Suri, 2006) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Nat
21 ChangRoberts Leader election in a ring (Chang & Rosemary, 1979) Stephan Merz ✔ Nat, Seq
22 DataPort Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016) Geoffrey Biggs, Noriaki Ando Int, Seq
23 detector_chan96 Chandra and Toueg’s eventually perfect failure detector Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Int, FinSet
24 DieHard A very elementary example based on a puzzle from a movie ✔ Nat
25 dijkstra-mutex Mutual exclusion algorithm (Dijkstra, 1965) Markus Alexander Kuppe ✔ Int
26 diskpaxos Disk Paxos (Gafni & Lamport, 2003) Giuliano Losa ✔ Int
27 egalitarian-paxos Leaderless replication protocol based on Paxos (Moraru et al., 2013) Iulian Moraru ✔ Nat, FinSet
28 ewd840 Termination detection in a ring (Dijkstra et al., 1986) Stephan Merz ✔ ✔ Nat
29 fastpaxos An extension of the classic Paxos algorithm, only PDF files (Lamport, 2006) Heidi Howard Nat, FinSet
30 fpaxos A variant of Paxos with flexible quorums (Howard et al., 2017) Heidi Howard ✔ Int
31 HLC Hybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014) Murat Demirbas ✔ Int
32 L1 Data center network L1 switch protocol, only PDF files (Thacker) Tom Rodeheffer FinSet, Nat, Seq
33 lamport_mutex Mutual exclusion (Lamport, 1978) Stephan Merz ✔ ✔ Nat, Seq
34 leaderless Leaderless generalized-consensus algorithms (Losa, 2016) Giuliano Losa ✔ FinSet, Int, Seq
35 losa_ap The assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018) Giuliano Losa ✔ FinSet, Nat, Seq
36 losa_rda Applying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014) Giuliano Losa FinSet, Nat, Seq
37 m2paxos Multi-leader consensus protocols (Peluso et al., 2016) Giuliano Losa ✔ Int, Seq, FinSet
38 mongo-repl-tla A simplified part of Raft in MongoDB (Ongaro, 2014) Siyuan Zhou ✔ FinSet, Nat, Seq
39 MultiPaxos The abstract specification of Generalized Paxos (Lamport, 2004) Giuliano Losa ✔ Int, FinSet
40 N-Queens The N queens problem Stephan Merz ✔ Nat, Seq
41 naiad Naiad clock protocol, only PDF files (Murray et al., 2013) Tom Rodeheffer ✔ Int, Seq, FinSet
42 nbacc_ray97 Asynchronous non-blocking atomic commit (Raynal, 1997) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Nat, FinSet
43 nbacg_guer01 On the hardness of failure-sensitive agreement problems (Guerraoui, 2001) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Nat, FinSet
44 nfc04 Non-functional properties of component-based software systems (Zschaler, 2010) Steffen Zschaler ✔ Real, Nat
45 Paxos Paxos consensus algorithm (Lamport, 1998) Leslie Lamport? ✔ Int, FinSet
46 Prisoners A puzzle was presented on an American radio program. ✔ Nat, FinSet
47 raft Raft consensus algorithm (Ongaro, 2014) Diego Ongaro ✔ FinSet, Nat, Seq
48 SnapshotIsolation Serializable snapshot isolation (Cahill et al., 2010) Michael J. Cahill, Uwe Röhm, Alan D. Fekete ✔ FinSet, Int, Seq
49 spanning Spanning tree broadcast algorithm in Attiya and Welch’s book Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Int
50 SpecifyingSystems Examples to accompany the book Specifying Systems (Lamport, 2002) ✔ all modules
51 Stones The same proble as CarTalkPuzzle ✔ FinSet, Int, Seq
52 sums_even Two proofs for showing that x+x is even, for any natural number x. ✔ ✔ Int
53 SyncConsensus Synchronized round consensus algorithm (Demirbas) Murat Demirbas ✔ FinSet, Int, Seq
54 Termination Channel counting algorithm (Mattern, 1987) Giuliano Losa ✔ FinSet, Bags, Nat
55 Tla-tortoise-hare Robert Floyd's cycle detection algorithm Lorin Hochstein ✔ Nat
56 tower_of_hanoi The well-known Towers of Hanoi puzzle. ✔ FinSet, Nat, Bit
57 transaction_commit Consensus on transaction commit (Gray & Lamport, 2006) Vasily Kuznetsov, Markus Alexander Kuppe ✔ Int
58 TransitiveClosure The transitive closure of a relation ✔ FinSet, Int, Seq
59 TwoPhase Two-phase handshaking Stephan Merz ✔ Nat
60 VoldemortKV Voldemort distributed key value store Murat Demirbas ✔ FinSet, Int, Seq

License

Every benchmark has initially the MIT license. If the authors want to change the license, we can create a special one for their benchmarks.

Support or Contact

Do you have any questions? Please contact Thanh-Hai Tran.