Understanding Reference Implementations
Relevant source files
The following files were used as context for generating this wiki page:This repository serves as a library of TLA+ specifications, but its value extends beyond abstract modeling. For several specifications, it provides reference implementations in programming languages like Java and Python. These implementations demonstrate how a high-level, formal TLA+ specification can be translated into concrete, executable code.
The process of implementing a formal spec reveals challenges in bridging the gap between an abstract model and a real-world system. This repository documents these challenges and showcases techniques like trace validation, where execution logs from an implementation are checked against the TLA+ spec to find divergences and bugs. This provides a powerful method for ensuring an implementation correctly adheres to its verified design.
Sources: README.md:4-7, specifications/ewd998/EWD998ChanTrace.md
The Spec-to-Implementation Workflow
The journey from an abstract TLA+ specification to a validated code implementation follows a structured process. This workflow leverages TLA+ and its tools not just for initial design verification but also for ensuring the final code is correct.
Sources: specifications/ewd998/EWD998ChanTrace.md
The following diagram illustrates the general workflow, using the EWD998 case study as an example.
- Specification: An algorithm or system is first modeled in TLA+ (e.g.,
EWD998Chan.tla). - Model Checking: The TLC model checker verifies properties like safety and liveness for the specification under a finite model.
- Implementation: The verified TLA+ spec is translated into a programming language (e.g.,
EWD998.java). - Logging: The implementation is instrumented to produce structured logs (e.g., JSON) that capture key state changes during execution.
- Trace Validation: A separate TLA+ specification (
EWD998ChanTrace.tla) is created. It uses the execution trace to see if the implementation's behavior is a valid behavior allowed by the original, high-level specification. TLC is used to perform this check.
Sources: specifications/ewd998/EWD998ChanTrace.md
Case Study: EWD998 Termination Detection (TLA+ to Java)
The EWD998 algorithm for termination detection in a ring provides a detailed example of the spec-to-implementation process, including the challenges encountered and the bugs found using trace validation.
Sources: specifications/ewd998/README.md:11-13, specifications/ewd998/EWD998ChanTrace.md
The TLA+ Specification (EWD998Chan.tla)
The EWD998Chan.tla specification models the algorithm at a high level. It uses abstract data structures and assumes atomicity for certain actions, which simplifies reasoning about correctness.
| TLA+ Variable | Description |
|---|---|
active | A function mapping each node to a boolean indicating if it's active. |
color | A function mapping each node to its color ("white" or "black"). |
counter | A function mapping each node to its message counter. |
inbox | A function mapping each node to a sequence of messages (its inbox). |
token | Represents the probe token, containing its color and message count. |
Sources: specifications/ewd998/EWD998Chan.tla
A key abstraction is that passing the token from one node to the next is modeled as a single, atomic step. This hides the complexity of network communication.
Sources: specifications/ewd998/EWD998ChanTrace.md:38-39
The Java Implementation (EWD998.java)
The Java implementation translates the abstract TLA+ concepts into concrete Java constructs. The implementation process was initially a straightforward translation, with some parts of the specification being copy-pasted.
Sources: specifications/ewd998/EWD998ChanTrace.md:2-4
The following class diagram shows the main components of the Java implementation.
The mapping from TLA+ variables to Java fields is direct:
active(TLA+) ->active(Javaboolean)color(TLA+) ->color(JavaString)counter(TLA+) ->counter(Javaint)inbox(TLA+) ->inbox(JavaLinkedBlockingQueue<Message>)token(TLA+) ->token(JavaMessageobject)
Sources: specifications/ewd998/impl/src/EWD998.java:51-60
Bridging the Abstraction Gap
Translating the spec to code required addressing several abstractions made in the TLA+ model.
- Concurrency: The Java implementation required a low-level
ReceiverThreadto handle network socket communication, a detail completely abstracted away in the TLA+ spec. - Atomicity: In
EWD998Chan.tla, passing a token is a single atomic action. In the implementation, this is non-atomic and involves network transmission. The trace validation spec had to account for this by allowing for explicit stuttering steps where variables remain unchanged. - State Logging: To enable trace validation, the implementation logs state to JSON at specific, consistent points: when a message is taken from the
inbox(conceptual receipt) and when a message is sent.
Sources: specifications/ewd998/EWD998ChanTrace.md:3-4, 13-17, 38-40
Trace Validation and Divergence Detection
Trace validation proved highly effective at finding subtle bugs and divergences between the implementation and the high-level specification. A EWD998ChanTrace.tla spec was used to check if the JSON log produced by the Java application corresponded to a valid behavior of EWD998Chan.tla.
This process uncovered several issues that were subsequently fixed.
| Divergence Found | Description | Resolution |
|---|---|---|
| Token Retention | A node receiving a token did not correctly retain it across a loop, causing a bug. | Fixed in the Java code after debugging. |
| Missing "trm" Messages | The implementation sent termination ("trm") messages not present in the original model. | The trace validation spec was updated to allow for these messages. |
| Self-Messaging | The implementation allowed a node to send a message to itself, which was not permitted by the high-level spec. | The implementation was modified to align with the spec. |
| Single-Node Edge Case | In a single-node system, the token did not appear to move, causing a validation failure. | The trace validation predicate IsInitiateToken was adjusted to handle this edge case. |
| Premature Probe | The initiator could start a new token round even if the previous one was conclusive. | The implementation logic was corrected to match the spec. |
Sources: specifications/ewd998/EWD998ChanTrace.md:7-8, 48-51, 53-55, 57-59, 66-68
The following diagram shows the trace validation flow.
Case Study: MultiPaxos SMR (TLA+ to Rust)
The MultiPaxos-SMR specification is another example that emphasizes a close relationship with a real-world implementation. It is designed as a "practical state machine replication (SMR) style" specification that models how a system would implement MultiPaxos for log replication.
Sources: specifications/MultiPaxos-SMR/README.md:1-3
This spec differs from more abstract Paxos specifications by including practical details:
- Explicit Log Replication: Servers explicitly replicate a log of instances, each holding a state machine command.
- Client-Driven Model: The number of client write/read commands are model inputs, making the model closer to a real system's workload.
- Client-View Linearizability: The key safety property is defined as linearizability from the client's perspective upon termination.
This TLA+ model corresponds to a Rust implementation in the summerset project, a protocol-generic distributed key-value store. This link between the formal model and the Rust code allows for high-confidence development.
Sources: specifications/MultiPaxos-SMR/README.md:13-21, 31-35
Conclusion
The examples within this repository demonstrate that TLA+ is more than a tool for abstract design. When combined with a disciplined implementation and validation workflow, it becomes a powerful framework for building correct distributed and concurrent systems. The process of translating a spec to code, and particularly validating the implementation's trace against the spec, provides strong guarantees that the final software adheres to its verified design, catching subtle bugs that might otherwise be missed.
Sources: README.md:4-7, specifications/ewd998/EWD998ChanTrace.md, specifications/MultiPaxos-SMR/README.md:1-3