I’ve been helping define some concurrent algorithms and I’m struggling with a number of issues: concurrent algorithms are difficult to design, they are often difficult to implement, and, even after they are designed, are difficult to guarantee that they are correct. This lead me into some research on formal specifications for algorithms, and how they can help. Finally, I settled on TLA+ as a viable tool for just such a problem.
What is TLA+
TLA+ is used to design, model, document, and verify concurrent systems, providing exhaustively testable pseudocode for building complex software systems. TLA stands for Temporal Logic of Actions and is based on formal temporal logic, which is a system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. TLA adds the concept of Actions to temporal logic, providing ways to formalize the actions used in concurrent systems.
Why TLA+
With a formal specification, such as TLA+, you express “what must go right” by explicitly specifying the correctness properties of a system, alongside the system’s operating environment. This approach is significantly less error prone than expressing “what might go wrong” using unit tests and quality assurance. Using a formal specification allows you to catch design bugs in your code before you implement an algorithm. It also serves as excellent documentation.
The TLA+ Ecosystem
TLA+ has a number of components. First, the language itself, which provides a verifiable specification of an algorithm. This is combined with a model checker, called the TLC model checker, that can exhaustively check the specification to make sure that it does what it says it does. TLC defines what the expected behaviour of a TLA+ specification is, what TLC should check, and what values to substitute for parameters in your specification. TLC checks that the state of your model is accurate before, during, and after the TLA+ algorithm runs. The last major component of the TLA+ ecosystem is TLAPS, the TLA+ proof system. The proof system mechanically checks TLA+ proofs as a collection of claims and assertions. TLAPS checks user-provided proofs of theorems and verifies that the hierarchy of claims indeed establishes the truth of the theorem.