Classic Concurrency Algorithms
Relevant source files
The following files were used as context for generating this wiki page:- README.md
- specifications/DiningPhilosophers/manifest.json
- specifications/ReadersWriters/manifest.json
- specifications/Bakery-Boulangerie/manifest.json
- specifications/lamport_mutex/manifest.json
- specifications/dijkstra-mutex/manifest.json
- specifications/ewd998/README.md
- specifications/ewd840/manifest.json
- specifications/locks_auxiliary_vars/README.md
- specifications/MultiPaxos-SMR/README.md
- specifications/PaxosHowToWinATuringAward/README.txt
This repository contains a collection of TLA+ specifications for classic concurrency and distributed algorithms. These examples serve as a comprehensive library for learning how to specify algorithms in TLA+, a corpus for testing TLA+ language tools, and a set of case studies for applying formal methods. The specifications are validated using tools like TLC (model checker), Apalache (symbolic model checker), and TLAPS (proof system).
Many specifications are written in PlusCal, a high-level algorithm language that translates to TLA+. This allows for a more familiar, pseudocode-like representation of the algorithms while still enabling rigorous formal verification.
Sources: README.md, CONTRIBUTING.md
Featured Algorithms
The repository includes a wide range of algorithms, many of which are foundational in the study of concurrent and distributed systems. The table below highlights several prominent examples related to concurrency.
| Name | Author(s) | PlusCal | TLAPS Proof | TLC Model |
|---|---|---|---|---|
| The Boulangerie Algorithm | Leslie Lamport, Stephan Merz | ✔ | ✔ | ✔ |
| Dijkstra's Mutual Exclusion Algorithm | Leslie Lamport | ✔ | ✔ | |
| Distributed Mutual Exclusion | Stephan Merz | ✔ | ✔ | |
| The Dining Philosophers Problem | Jeff Hemphill | ✔ | ✔ | |
| The Readers-Writers Problem | Isaac DeFrain | ✔ | ||
| EWD840: Termination Detection in a Ring | Stephan Merz | ✔ | ✔ | |
| EWD998: Termination Detection (Async) | Stephan Merz, Markus Kuppe | (✔) | ✔ | ✔ |
| Peterson Lock Refinement | Jarod Differdange | ✔ | ✔ | ✔ |
| The Paxos Protocol | Leslie Lamport | (✔) | ✔ | |
| MultiPaxos in SMR-Style | Guanzhou Hu | ✔ | ✔ |
Sources: README.md
Mutual Exclusion Algorithms
Mutual exclusion is a fundamental problem in concurrency, ensuring that no two processes are in their critical section at the same time. This repository contains several classic solutions.
The Bakery (Boulangerie) Algorithm
This algorithm provides a solution to the mutual exclusion problem for N processes. The Bakery-Boulangerie specification includes both TLA+ and PlusCal versions, along with a formal proof checked by TLAPS and models verified by TLC.
- Bakery.tla: Contains a PlusCal specification and a TLAPS-checked proof with a runtime of approximately 20 seconds.
- Boulanger.tla: A variant of the Bakery algorithm, also with a PlusCal spec and a 30-second proof.
- MCBakery.tla / MCBoulanger.tla: Models for TLC checking, with runtimes of 10 seconds and 1 minute, respectively.
Sources: specifications/Bakery-Boulangerie/manifest.json
Peterson's Algorithm and Refinement
Peterson's algorithm is a simpler mutual exclusion solution for two processes. The locks_auxiliary_vars specification demonstrates how this concrete algorithm can be proven as a refinement of a more abstract lock specification. This is achieved using auxiliary variables to bridge the gap between the implementation and the abstract spec.
The diagram below shows the refinement relationship demonstrated in the specification.
This diagram illustrates the two-way refinement proof approach for Peterson's algorithm.
Lock.tla: An abstract lock where acquisition is atomic.Peterson.tla: The PlusCal implementation of Peterson's algorithm. It proves refinement fromLock!Spec.LockHS.tla: An extended version of the abstract lock using history and stuttering variables to allow a refinement proof towardsPeterson!Spec.
Sources: specifications/locks_auxiliary_vars/README.md
Other Mutual Exclusion Algorithms
- Dijkstra's Mutual Exclusion: A PlusCal specification of Dijkstra's algorithm for mutual exclusion.
Sources: specifications/dijkstra-mutex/manifest.json - Lamport's Distributed Mutual Exclusion: A TLA+ specification of Lamport's timestamp-based algorithm for distributed mutual exclusion, complete with a formal proof.
Sources: specifications/lamport_mutex/manifest.json
Classic Synchronization Problems
The Dining Philosophers
This is a classic synchronization problem used to illustrate challenges like deadlock and starvation. The specification is marked as beginner-friendly and uses PlusCal, making it an accessible example for newcomers to TLA+. It is verified using a TLC model.
Sources: README.md, specifications/DiningPhilosophers/manifest.json
The Readers-Writers Problem
This problem concerns access to a shared resource by multiple processes, where some ("readers") only read the data and others ("writers") modify it. The goal is to allow multiple readers simultaneously but only a single writer at any time. The repository contains a TLA+ specification with a TLC model to verify its properties.
Sources: README.md, specifications/ReadersWriters/manifest.json
Termination Detection
Termination detection is crucial in distributed systems to determine if a distributed computation has finished. The repository contains specifications for Dijkstra's algorithms for this purpose.
EWD840 and EWD998
EWD840 describes a termination detection algorithm for a ring topology with synchronous message passing. EWD998 extends this to support asynchronous message delivery. The specifications demonstrate a clear refinement hierarchy, where more concrete implementations are proven to satisfy the properties of more abstract ones.
The refinement hierarchy is as follows:
This diagram shows how the termination detection specifications refine each other, from abstract to concrete.
The ewd998 specification also explores the performance of different algorithmic variants by simulating them and collecting statistics on the number of steps required to detect termination. Four variants are analyzed:
| Variant | Description |
|---|---|
pt1 | An active node may pass the token if the node is black/tainted. |
pt2 | An active node may pass the token if the token is black/tainted. |
pt3 | Return the token to the initiator if the node is black. |
pt4 | Return the token to the initiator if the token is black. |
Analysis showed that variants pt3 and pt4 significantly increased the number of token passes required in the worst case, making them less efficient than the original algorithm.
Sources: specifications/ewd998/README.md, specifications/ewd840/manifest.json
Consensus Algorithms
Consensus is a fundamental problem in fault-tolerant distributed systems. The repository includes several specifications of the Paxos algorithm, a foundational protocol for achieving consensus.
Paxos
The PaxosHowToWinATuringAward specification provides a step-by-step introduction to Paxos, breaking it down into three parts: Consensus, Voting, and Paxos. This is designed as an educational resource to help users understand the algorithm and how to model it in TLA+.
Sources: specifications/PaxosHowToWinATuringAward/README.txt
MultiPaxos for State Machine Replication (SMR)
The MultiPaxos-SMR specification provides a practical, SMR-style model of MultiPaxos. It is designed to be much closer to a real-world implementation than more abstract specifications.
Key features include:
- Servers explicitly replicate a log of commands.
- The number of client read/write commands are model inputs.
- An explicit termination condition is defined, allowing for liveness checks (via deadlock freedom).
- Safety is checked via a client-viewed linearizability property.
The specification is written in PlusCal and includes models for checking with TLC.