TLA+ Examples

The SnapshotIsolation specification implements the Serializable Snapshot Isolation algorithm described by Cahill, Röhm, and Fekete. It is designed to model serializable isolation for snapshot databases.

Key Technical Details

• Authors: Michael J. Cahill, Uwe Röhm, Alan D. Fekete.
• Original Paper: Serializable isolation for snapshot databases (ACM TODS 2009).
• Extended Modules: Uses FinSet, Int, and Seq modules.
• Computation Model: Uses a Write-rejection model.
• Verified Properties: The specification includes properties checked with the TLC model checker, specifically termination and correctness.

The spanning specification is a TLA+ model used for benchmarking or research purposes. It is characterized by the following metadata:

• Authors: Thanh Hai Tran, Igor Konnov, Josef Widder
• Original Paper: Available in the tlabenchmarks repository.
• Extended Modules: Uses the Int module.
• Computation Model: Assumes a model with no faults.
• Verified Properties: The following properties are checked using the TLC model checker:
  • OneParent
  • termination

The losa_ap specification is an implementation of 'The Assignment Problem' as described by Delporte-Gallet et al. (2018). It is designed to model assignment problems in distributed systems.

Key Details

• Authors: Giuliano Losa
• Computation Model: Models system behavior under crashes.
• Extended Modules: Relies on FinSet, Nat, and Seq modules.
• Properties Verified: The specification includes properties checked with the TLC model checker, specifically:
  • fairness
  • consistency
  • correctness
  • termination

The Tencent-Paxos-TLA specification is an implementation of the Tencent Paxos protocol, based on the research paper "PaxosStore: high-availability storage made practical in WeChat".

Key characteristics of this specification:

• Authors: Xingchen Yi, Hengfeng Wei
• Extended Modules: Uses Integers and FiniteSets modules.
• Computation Models: Models system failures including node crashes and network issues such as lost or duplicated messages.
• Properties Verified: Uses the TLC model checker to verify properties such as Consistency.

The bcastFolklore specification is an implementation of concepts from the paper "Unreliable failure detectors for reliable distributed systems" by Chandra and Toueg (1996). It models distributed systems using a clean crashes computation model.

Key technical details:

• Authors: Thanh Hai Tran, Igor Konnov, Josef Widder.
• Extended Modules: Uses the Nat module.
• Properties Verified: The specification uses TLC to check for correctness, relay, and unforgeability.
• Formal Proofs: The implementation of the Alternative specification is verified using TLAPS (TLA+ Proof System).

The c1cs specification implements the 'Consensus in one communication step' algorithm described by Brasileiro, Francisco, et al. (2001). It is designed to demonstrate consensus protocols under a computation model featuring 'clean crashes'.

Key details:

• Authors: Thanh Hai Tran, Igor Konnov, Josef Widder
• Extended Modules: Int, FinSet
• Computation Model: clean crashes
• Verified Properties: The specification includes TLC checks for validity, agreement, weak-agreement, and termination.

The tlaplus/examples repository is a collection of TLA+ specifications and models used for various purposes:

• A library for learning how to specify algorithms in TLA+.
• A corpus for developing and testing TLA+ language tools.
• A collection of case studies for formal specification applications.

All specifications are located in the specifications directory. Each specification directory contains a manifest.json file providing detailed metadata about the spec, such as its difficulty level, whether it includes a PlusCal variant, and which verification tools (TLC, Apalache, or TLAPS) it supports.

The cbc_max example is a TLA+ specification based on the paper "Evaluating the condition-based approach to solve consensus" by Mostéfaoui, Achour, et al. (2003). It models a consensus protocol using a condition-based approach.

Key technical details:

• Authors: Thanh Hai Tran, Igor Konnov, Josef Widder
• Computation Model: Byzantine
• Extended Modules: Int, FinSet
• Properties Verified with TLC:
  • validity
  • agreement
  • termination

The SyncConsensus specification implements a Synchronized Round Consensus Algorithm. It is based on research by Murat Demirbas and is designed to model consensus in environments where computation models include crashes.

Key details for users:

• Authorship: Murat Demirbas
• Original Paper: TLA+/PlusCal modeling of Synchronized Round Consensus Algorithm
• Dependencies: Uses extended modules FinSet, Int, and Seq.
• Properties Verified: The specification includes properties checked with the TLC model checker, specifically agreement, Syncterm, and Term.

The losa_rda specification is an implementation of concepts from Giuliano Losa's PhD thesis, "Modularity in the design of robust distributed algorithms." It demonstrates modularity in distributed algorithms and includes checks for correctness and refinement mapping using the TLC model checker.

Key characteristics:

• Computation Models: Supports scenarios involving node crashes and lost messages.
• Extended Modules: Utilizes FinSet, Nat, and Seq modules.
• Properties Verified: Uses TLC to verify correctness and refinement mappings.
• Format: The source documentation is provided in PDF format.

The fpaxos specification is a TLA+ implementation of the Flexible Paxos algorithm, originally authored by Heidi Howard. It explores quorum intersection to provide flexibility in Paxos implementations.

Key Details

• Original Paper: Flexible Paxos: Quorum Intersection Revisited (Howard, Malkhi, and Spiegelman, 2017).
• Extended Modules: Uses the Int module.
• Computation Models: The specification accounts for node crashes and lost or duplicated messages.
• Properties Verified with TLC:
  • agreed: Ensures consensus is reached.
  • SafeValue: Ensures safety properties regarding the values chosen.

To use this specification, you can find the TLA+ files in the fpaxos repository.

This specification implements distributed termination detection algorithms based on research by Devendra Kumar (1985) and Friedemann Mattern (1987). It is designed for asynchronous computation models without faults.

Key technical details:

• Extended Modules: Uses Integers, FiniteSets, Apalache, and Sequences.
• Verification: Some properties are checked using the Apalache model checker, specifically an inductive invariant implying safety (verified for 5 processes).