Skip to content

A collection of TLA+ specifications of varying complexities

License

Notifications You must be signed in to change notification settings

nano-o/TLA--Examples

 
 

Repository files navigation

TLA+ Examples

Gitpod ready-to-code Validate Specs & Models

This is a repository of TLA+ specifications and models covering applications in a variety of fields. It serves as:

  • a comprehensive example library demonstrating how to specify an algorithm in TLA+
  • a diverse corpus facilitating development & testing of TLA+ language tools
  • a collection of case studies in the application of formal specification in TLA+

All TLA+ specs can be found in the specifications directory. The table below lists all specs and their features, such as whether they are suitable for beginners or use PlusCal. The manifest.json file is the source of truth for this table, and is a detailed human- & machine-readable description of the specs & their models. Its schema is manifest-schema.json. All specs in this repository are subject to CI validation to ensure quality.

Examples Included Here

Here is a list of specs included in this repository, with links to the relevant directory and flags for various features:

Name Author(s) Beginner TLAPS Proof PlusCal TLC Model Apalache
Learn TLA⁺ Proofs Andrew Helwer
Teaching Concurrency Leslie Lamport
Boyer-Moore Majority Vote Stephan Merz
Proof x+x is Even Stephan Merz
The N-Queens Puzzle Stephan Merz
The Dining Philosophers Problem Jeff Hemphill
The Car Talk Puzzle Leslie Lamport
The Die Hard Problem Leslie Lamport
The Prisoners & Switches Puzzle Leslie Lamport
Specs from Specifying Systems Leslie Lamport
The Tower of Hanoi Puzzle Markus Kuppe, Alexander Niederbühl
Missionaries and Cannibals Leslie Lamport
The Coffee Can Bean Problem Andrew Helwer
Stone Scale Puzzle Leslie Lamport
The Boulangerie Algorithm Leslie Lamport, Stephan Merz
Misra Reachability Algorithm Leslie Lamport
Loop Invariance Leslie Lamport
EWD840: Termination Detection in a Ring Stephan Merz
EWD998: Termination Detection in a Ring with Asynchronous Message Delivery Stephan Merz, Markus Kuppe
The Paxos Protocol Leslie Lamport
Asynchronous Reliable Broadcast Thanh Hai Tran, Igor Konnov, Josef Widder
Distributed Mutual Exclusion Stephan Merz
Two-Phase Handshaking Leslie Lamport, Stephan Merz
Paxos (How to Win a Turing Award) Leslie Lamport
Dijkstra's Mutual Exclusion Algorithm Leslie Lamport
The Echo Algorithm Stephan Merz
The TLC Safety Checking Algorithm Markus Kuppe
EWD687a: Detecting Termination in Distributed Computations Stephan Merz, Leslie Lamport, Markus Kuppe
The Slush Protocol Andrew Helwer
Minimal Circular Substring Andrew Helwer
Snapshot Key-Value Store Andrew Helwer, Murat Demirbas
Chang-Roberts Algorithm for Leader Election in a Ring Stephan Merz
Resource Allocator Stephan Merz
Transitive Closure Stephan Merz
Sliding Block Puzzle Mariusz Ryndzionek
Single-Lane Bridge Problem Younes Akhouayri
Huang's Algorithm Markus Kuppe
The Knuth-Yao Method Ron Pressler, Markus Kuppe
EWD 426: Token Stabilization Murat Demirbas, Markus Kuppe
Multi-Car Elevator System Andrew Helwer
Nano Blockchain Protocol Andrew Helwer
Software-Defined Perimeter Luming Dong, Zhi Niu
Simplified Fast Paxos Lim Ngian Xin Terry, Gaurav Gandhi
Checkpoint Coordination Andrew Helwer
Finitizing Monotonic Systems Andrew Helwer
The Readers-Writers Problem Isaac DeFrain
Einstein's Riddle Isaac DeFrain
Asynchronous Byzantine Consensus Thanh Hai Tran, Igor Konnov, Josef Widder
Folklore Reliable Broadcast Thanh Hai Tran, Igor Konnov, Josef Widder
The Bosco Byzantine Consensus Algorithm Thanh Hai Tran, Igor Konnov, Josef Widder
Consensus in One Communication Step Thanh Hai Tran, Igor Konnov, Josef Widder
Condition-Based Consensus Thanh Hai Tran, Igor Konnov, Josef Widder
One-Step Consensus with Zero-Degradation Thanh Hai Tran, Igor Konnov, Josef Widder
Failure Detector Thanh Hai Tran, Igor Konnov, Josef Widder
SWMR Shared Memory Disk Paxos Leslie Lamport, Giuliano Losa
Asynchronous Non-Blocking Atomic Commit Thanh Hai Tran, Igor Konnov, Josef Widder
Asynchronous Non-Blocking Atomic Commitment with Failure Detectors Thanh Hai Tran, Igor Konnov, Josef Widder
Spanning Tree Broadcast Algorithm Thanh Hai Tran, Igor Konnov, Josef Widder
Transaction Commit Models Leslie Lamport, Jim Gray
Span Tree Exercise Leslie Lamport
The Cigarette Smokers Problem Mariusz Ryndzionek
Conway's Game of Life Mariusz Ryndzionek
Chameneos, a Concurrency Game Mariusz Ryndzionek
TLA⁺ Level Checking Leslie Lamport
PCR Testing for Snippets of DNA Martin Harrison

Examples Elsewhere

Here is a list of specs stored in locations outside this repository, including submodules. They are not covered by CI testing so it is possible they contain errors, the reported details are incorrect, or they are no longer available. Ideally these will be moved into this repo over time.

Name Description Author(s) TLAPS Proof? TLC Model? PlusCal? Apalache?
2PCwithBTM A modified version of P2TCommit (Gray & Lamport, 2006) Murat Demirbas
802.16 IEEE 802.16 WiMAX Protocols Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou
acp-nb Non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) Stephan Merz
acp-nb-wrong Wrong version of the non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) Stephan Merz
acp-sb Non-blocking atomic commitment with a simple broadcast (Babaoğlu & Toueg, 1993) Stephan Merz
async-comm The diversity of asynchronous communication (Chevrou et al., 2016) Florent Chevrou, Aurélie Hurault, Philippe Quéinnec
byihive Based on RFC3506 - Requirements and Design for Voucher Trading System (Fujimura & Eastlake) Santhosh Raju
byzpaxos Byzantizing Paxos by Refinement (Lamport, 2011) Leslie Lamport
Caesar Multi-leader generalized consensus protocol (Arun et al., 2017) Giuliano Losa
CASPaxos An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov) Tobias Schottdorf
DataPort Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016) Geoffrey Biggs, Noriaki Ando
egalitarian-paxos Leaderless replication protocol based on Paxos (Moraru et al., 2013) Iulian Moraru
fastpaxos An extension of the classic Paxos algorithm, only PDF files (Lamport, 2006) Leslie Lamport
fpaxos A variant of Paxos with flexible quorums (Howard et al., 2017) Heidi Howard
HLC Hybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014) Murat Demirbas
L1 Data center network L1 switch protocol, only PDF files (Thacker) Tom Rodeheffer
leaderless Leaderless generalized-consensus algorithms (Losa, 2016) Giuliano Losa
losa_ap The assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018) Giuliano Losa
losa_rda Applying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014) Giuliano Losa
m2paxos Multi-leader consensus protocols (Peluso et al., 2016) Giuliano Losa
mongo-repl-tla A simplified part of Raft in MongoDB (Ongaro, 2014) Siyuan Zhou
MultiPaxos The abstract specification of Generalized Paxos (Lamport, 2004) Giuliano Losa
naiad Naiad clock protocol, only PDF files (Murray et al., 2013) Tom Rodeheffer
nfc04 Non-functional properties of component-based software systems (Zschaler, 2010) Steffen Zschaler
raft Raft consensus algorithm (Ongaro, 2014) Diego Ongaro
SnapshotIsolation Serializable snapshot isolation (Cahill et al., 2010) Michael J. Cahill, Uwe Röhm, Alan D. Fekete
SyncConsensus Synchronized round consensus algorithm (Demirbas) Murat Demirbas
Termination Channel-counting algorithm (Kumar, 1985) Giuliano Losa
Tla-tortoise-hare Robert Floyd's cycle detection algorithm Lorin Hochstein
VoldemortKV Voldemort distributed key value store Murat Demirbas
Tencent-Paxos PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017) Xingchen Yi, Hengfeng Wei
Paxos Paxos
Lock-Free Set PlusCal spec of a lock-Free set used by TLC Markus Kuppe
ParallelRaft A variant of Raft Xiaosong Gu, Hengfeng Wei, Yu Huang
CRDT-Bug CRDT algorithm with defect and fixed version Alexander Niederbühl
asyncio-lock Bugs from old versions of Python's asyncio lock Alexander Niederbühl
Raft (with cluster changes) Raft with cluster changes, and a version with Apalache type annotations but no cluster changes George Pîrlea, Darius Foom, Brandon Amos, Huanchen Zhang, Daniel Ricketts
MET for CRDT-Redis Model-check the CRDT designs, then generate test cases to test CRDT implementations Yuqi Zhang
Parallel increment Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry Chris Jensen
The Streamlet consensus algorithm Specification and model-checking of both safety and liveness properties of Streamlet with TLC Giuliano Losa
Petri Nets Instantiable Petri Nets with liveness properties Eugene Huang
CRDT Specifying and Verifying CRDT Protocols Ye Ji, Hengfeng Wei
Azure Cosmos DB Consistency models provided by Azure Cosmos DB Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe
Blocking Queue BlockingQueue Markus Kuppe

License

The repository is under the MIT license and you are encouraged to publish your spec under a similarly-permissive license. However, your spec can be included in this repo along with you own license if you wish.

Support or Contact

Do you have any questions or comments? Please open an issue or send an email to the TLA+ group.

Contributing

Do you have your own case study or TLA+ specification you'd like to share with the community? Follow these instructions:

  1. Fork this repository and create a new directory under specifications with the name of your spec
  2. Place all TLA+ files in the directory, along with their .cfg model files; you are encouraged to include at least one model that completes execution in less than 10 seconds
  3. Ensure name of each .cfg file matches the .tla file it models, or has its name as a prefix; for example SpecName.tla can have the models SpecName.cfg and SpecNameLiveness.cfg, etc.
  4. Consider including a README.md in the spec directory explaining the significance of the spec with links to any relevant websites or publications, or integrate this info as comments in the spec itself
  5. Add an entry to the table of specs included in this repo, summarizing your spec and its attributes

Adding Spec to Continuous Integration

To combat bitrot, it is important to add your spec and model to the continuous integration system. To do this, you'll have to update the manifest.json file with machine-readable records of your spec files. If this process doesn't work for you, you can alternatively modify the .ciignore file to exclude your spec from validation. Otherwise, follow these directions:

  1. Ensure you have Python 3.11+ installed
  2. Download & extract tree-sitter-tlaplus (zip, tar.gz) to the root of the repository; ensure the extracted folder is named tree-sitter-tlaplus
  3. Open a shell and navigate to the repo root; ensure a C++ compiler is installed and on your path
    • On Windows, this might entail running the below script from the visual studio developer command prompt
  4. It is considered best practice to create & initialize a Python virtual environment to preserve your system package store; run python -m venv . then source ./bin/activate on Linux & macOS or .\Scripts\activate.bat on Windows (run deactivate to exit)
  5. Run pip install -r .github/scripts/requirements.txt
  6. Run python .github/scripts/generate_manifest.py
  7. Locate your spec's entry in the manifest.json file and ensure the following fields are filled out:
    • Spec title: an appropriate title for your specification
    • Spec description: a short description of your specification
    • Spec source: if this spec was first published elsewhere, provide a link to this location
    • Spec authors: a list of people who authored the spec
    • Spec tags:
      • "beginner" if your spec is appropriate for TLA+ newcomers
    • Model runtime: approximate model runtime on an ordinary workstation, in "HH:MM:SS" format
    • Model size:
      • "small" if the model can be executed in less than 10 seconds
      • "medium" if the model can be executed in less than five minutes
      • "large" if the model takes more than five minutes to execute
    • Model mode:
      • "exhaustive search" by default
      • {"simulate": {"traceCount": N}} for a simulation model
      • "generate" for model trace generation
    • Model result:
      • "success" if the model completes successfully
      • "safety failure" if the model violates an invariant
      • "liveness failure" if the model fails to satisfy a liveness property
      • "deadlock failure" if the model encounters deadlock
    • Other fields are auto-generated by the script; if you are adding an entry manually, ensure their values are present and correct (see other entries or the manifest-schema.json file)

Before submitted your changes to run in the CI, you can quickly check your manifest.json for errors and also check it against manifest-schema.json at https://www.jsonschemavalidator.net/.

About

A collection of TLA+ specifications of varying complexities

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • TLA 96.6%
  • TeX 2.9%
  • Other 0.5%