Case Study: EWD998 Java Implementation
Relevant source files
The following files were used as context for generating this wiki page:
This document details the process of implementing Shmuel Safra's EWD998 termination detection algorithm in Java and validating it against its formal TLA+ specification. The core of this case study is the use of trace validation, a technique where execution logs from the Java implementation are model-checked against the high-level TLA+ specification to ensure conformance and detect subtle bugs.
The EWD998 algorithm is an extension of EWD840 that supports asynchronous message delivery in a ring topology. The TLA+ specifications for this algorithm are structured in a refinement hierarchy, providing layers of abstraction from the core logic down to a version with explicit message channels, which serves as the basis for the implementation.
Sources: specifications/ewd998/README.md, specifications/ewd998/EWD998ChanTrace.md
TLA+ Specification Hierarchy
The Java implementation is based on the EWD998Chan.tla specification. This spec is part of a larger refinement hierarchy that formally proves the algorithm's correctness. The hierarchy demonstrates how the concrete implementation with message channels (EWD998Chan) refines the more abstract algorithm (EWD998), which in turn refines the general properties of asynchronous termination detection.
This diagram shows the refinement relationship between the different TLA+ specifications for EWD840 and EWD998.
Sources: specifications/ewd998/README.md
Implementation Process
The initial Java implementation was developed in approximately two hours, based directly on the EWD998Chan.tla specification. The process was largely a straightforward translation from the TLA+ logic to Java code. The primary exception was the low-level network receiver thread, which is abstracted away in the TLA+ model but requires explicit implementation in a real system. Initially, a custom wire format was used, but it was later replaced with JSON to avoid error-prone ad-hoc parsing.
Sources: specifications/ewd998/EWD998ChanTrace.md
Trace Validation Methodology
Trace validation was used to verify that the Java implementation's behavior conforms to the EWD998Chan.tla specification. Instead of trying to model the entire Java program in TLA+, this approach checks if a recorded execution trace (a log file) corresponds to a valid behavior allowed by the high-level specification.
The following diagram illustrates the trace validation workflow.
The core of this method is a TLA+ specification (EWD998ChanTrace.tla) that uses state and action constraints to process the trace. For each entry in the trace, TLC attempts to find a corresponding step in the high-level specification that could produce that observation. If every entry in the trace can be matched to a step in a single, valid TLA+ behavior, the trace is accepted.
Sources: specifications/ewd998/EWD998ChanTrace.md, specifications/ewd998/manifest.json
Challenges in Trace Validation
Several challenges were encountered during the development of the trace validation process.
- Partial Traces: The execution log is a highly partial observation of the system's state. It does not contain the values of all variables at every step. Attempting to axiomatically define the missing values using non-determinism proved to be impractical for TLC to handle.
- Lack of Global Clock: In a distributed system, there is no global clock, meaning log entries from different nodes may not be causally ordered. The canonical solution, vector clocks, was modeled in
EWD998ChanID.tlato correctly order events for visualization with ShiViz. - Atomicity Mismatch: Actions that are modeled as atomic in TLA+ (e.g., a node passing a token) are not atomic in the implementation. This was addressed by introducing explicit stuttering steps in the validation specification, allowing the model to remain in the same state while the implementation completes its non-atomic operation.
Sources: specifications/ewd998/EWD998ChanTrace.md
Divergences Found via Trace Validation
The trace validation process was highly effective, uncovering several divergences between the implementation and the specification. These findings led to fixes in either the Java code or the validation logic.
| Divergence / Bug | Description | Resolution | Source |
|---|---|---|---|
| 1. Token Retention Bug | A node receiving a token did not correctly retain it across a while loop. | Fixed in the Java code after discovery during initial debugging runs. | Debugging and Error Resolution |
| 2. Unlogged Deactivation | Node deactivation was not logged, causing validation failure when a seemingly active node passed a token. | The validation spec was updated to compose actions (Deactivate \cdot PassToken) to model the unobserved state change. | Handling Unlogged Deactivation Events |
| 3. Extra "trm" Messages | The implementation sent termination ("trm") messages that were not part of the EWD998 model. | The TraceNextConstraint in the validation spec was updated to allow for these messages using finite stuttering. | Handling Termination Messages |
| 4. Self-Messaging | The implementation allowed a node to send a message to itself, which the specification forbade. | The Java implementation was modified to prevent self-messaging, aligning it with the specification. | SendMsg Action |
| 5. Single-Node Edge Case | In a single-node system, the token did not appear to move, causing a validation mismatch. | The IsInitiateToken predicate in the validation spec was adjusted to handle this edge case. | Single node configuration |
| 6. Incorrect Re-initiation | The initiator would start a new token round even when the previous one was conclusive. | The implementation logic was corrected to prevent this unnecessary and incorrect behavior. | Final Implementation |
Sources: specifications/ewd998/EWD998ChanTrace.md
Logging for Validation and Visualization
A structured JSON logging format was crucial for both trace validation and visualization.
- Logging Points: To ensure consistent state, logging occurs at two key points: when a message is conceptually received (i.e., taken from the inbox queue) and when a message is sent.
- ShiViz Integration: To visualize traces with the ShiViz tool, vector clocks were implemented and included in the logs. The JSON format was updated to include the node's identity and the vector clock, enabling causal ordering of events. The following regex was used to parse the logs for visualization.
^{"event":"(<|>|d)","node":(?<host>[0-9]?),"pkt":{("snd":(?<src>[0-9]?),"rcv":(?<rcv>[0-9]?),"msg":(?<event>({"type":"tok","q":-?[0-9]*,"color":"(white|black)"}|{"type":"(pl|trm|w|d)"})),|)"vc":(?<clock>.*)}}
Sources: specifications/ewd998/EWD998ChanTrace.md, specifications/ewd998/README.md
Conclusion
This case study successfully demonstrates a powerful, practical technique for ensuring a real-world implementation conforms to its formal TLA+ specification. By using TLC to model-check execution traces from a Java program, the process bridged the gap between abstract specification and concrete code. This validation method proved highly effective, identifying several subtle bugs and logical divergences that could have been easily missed by traditional testing methods, ultimately leading to a more correct and robust implementation of the EWD998 algorithm.