Troubleshooting Common Errors
Relevant source files
The following files were used as context for generating this wiki page:
This document provides guidance on understanding, identifying, and troubleshooting common errors within the TLA+ specifications in this repository. The project uses the TLA+ model checker, TLC, to verify algorithms, and a key part of this process is analyzing the failures it reports. These failures can indicate flaws in the algorithm's design, errors in the TLA+ specification, or divergences between a specification and its implementation.
The repository intentionally includes specifications that fail in interesting ways. These serve as educational examples and as regression tests for TLA+ tooling. Understanding how to interpret these failures is crucial for both contributing to this repository and for applying formal methods to other projects.
Sources: README.md:3-8, CONTRIBUTING.md:12-13
Understanding Model Checking Failures with TLC
The primary tool for finding errors in TLA+ specifications is the TLC model checker. When TLC runs on a model, it explores the state space defined by the specification. If it finds a state that violates a specified property (like an invariant or a liveness property), it halts and produces an error trace.
Sources: specifications/PaxosHowToWinATuringAward/README.txt:40-44
Types of Failures
The manifest.json files within each specification directory categorize models by their expected result, including several types of failures. These keywords are useful for searching the repository for specific error examples.
| Failure Type | Description |
|---|---|
safety failure | The model violates an invariant (a property that must always be true). This is a common failure type. |
liveness failure | The model fails to satisfy a liveness property (a property that must eventually become true). |
deadlock failure | The model reaches a state from which no further progress can be made (no action is enabled). |
assumption failure | The model violates an assumption made about the environment or its inputs. |
Sources: README.md:21-22, CONTRIBUTING.md:58-62
TLC Debugging Workflow
The goal of running TLC is to determine if an algorithm is correct. A reported error is most valuable when it reveals a genuine flaw in the algorithm rather than a simple mistake in the TLA+ specification.
The following diagram illustrates the typical workflow for using TLC to debug an algorithm.
This diagram shows the iterative process of writing a specification, checking it with TLC, and analyzing the results to refine either the specification or the algorithm itself.
Sources: specifications/PaxosHowToWinATuringAward/README.txt:70-76
Identifying Failing Specifications
The repository is structured to make finding specific examples of failing models straightforward.
Searching for Failures
You can search for specifications that demonstrate particular failures by using grep on the command line to search through the manifest.json files.
# Find all models expected to have a safety failure
ls specifications/*/manifest.json | xargs grep -l "safety failure"
This command leverages the structured metadata in each specification's manifest to quickly locate relevant examples.
Sources: README.md:18-22
Example Failing Models
The following table lists some specifications from the repository that are configured to produce an error.
| Specification | Model File | Expected Failure |
|---|---|---|
SDP_Verification | specifications/SDP_Verification/SDP_Attack_Spec/MC.cfg | safety failure |
ewd687a | specifications/ewd687a/EWD687a_anim.cfg | safety failure |
MissionariesAndCannibals | specifications/MissionariesAndCannibals/MissionariesAndCannibals.cfg | safety failure |
Sources: specifications/SDP_Verification/manifest.json:28-34, specifications/ewd687a/manifest.json:20-26, specifications/MissionariesAndCannibals/manifest.json:13-19
Case Study: Debugging Divergences in EWD998
The ewd998 specification provides a detailed log of debugging an implementation against its TLA+ specification. This process, called trace validation, revealed several "divergences" where the implementation's behavior did not match the high-level specification.
The core idea of trace validation is to check if a trace (log file) from a real implementation corresponds to a valid behavior in the high-level TLA+ model.
Sources: specifications/ewd998/EWD998ChanTrace.md:19-21, specifications/ewd998/EWD998ChanTrace.md:28-32
Trace Validation Process
The following diagram shows how an implementation trace is validated against the TLA+ specification using TLC.
This sequence shows TLC attempting to match each step of a logged execution trace to a possible behavior in the formal specification. A failure to match indicates a divergence.
Sources: specifications/ewd998/EWD998ChanTrace.md:28-32
Discovered Divergences
The trace validation process for EWD998 uncovered several bugs and inconsistencies between the code and the formal model.
| Divergence | Description | Resolution |
|---|---|---|
| Token Retention | A node receiving a token did not correctly retain it. This was a translation error from the spec. | The bug was fixed in the Java code after debugging. |
| Termination Messages | The implementation sent termination ("trm") messages that were not modeled in the high-level spec. | The trace validation spec was updated to allow for these messages via finite stuttering. |
| 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 stricter behavior of the specification. |
| Conclusive Round | The initiator would start a new token round even if the previous round was conclusive. | The implementation logic was corrected to match the specification, eliminating the divergence. |
Sources: specifications/ewd998/EWD998ChanTrace.md:9-10, specifications/ewd998/EWD998ChanTrace.md:52-56, specifications/ewd998/EWD998ChanTrace.md:58-61, specifications/ewd998/EWD998ChanTrace.md:70-73
Inducing Failures for Verification
A powerful technique for gaining confidence in a specification and its properties is to intentionally introduce a bug and verify that TLC finds the expected error. If TLC does not report an error after a deliberate modification, it could mean the property being checked is too weak or the specification is not modeling the system as intended.
Sources: specifications/PaxosHowToWinATuringAward/README.txt:74-76, specifications/MultiPaxos-SMR/README.md:12-13
Examples of Induced Failures
The MultiPaxos-SMR specification provides clear examples of how to induce failures:
- Linearizability Failure: In the
HandleAcceptRepliesaction, changing theawaitcondition from>= MajorityNumto>= MajorityNum - 1weakens the quorum requirement. This should, and does, cause TLC to report a violation of the linearizability property. - Deadlock Failure: In the
HandleAcceptaction, commenting out theSendaction forAcceptReplyMsgprevents a node from replying. This will eventually lead to a state where other nodes are waiting for replies that will never arrive, causing a deadlock.
These exercises confirm that the properties are correctly specified and that TLC is capable of detecting these classes of errors in the model.