Mechanical Verification of Concurrent Systems with TLA

When I developed TLA, I realized that, for the first time, I had a formalism that really was completely formal–so formal that mechanically checking TLA proofs should be straightforward. Working out a tiny example (the specification and trivial implementation of mutual exclusion) using the LP theorem prover, I confirmed that this was the case. I used LP mainly because we had LP experts at SRC–namely, Jim Horning and Jim Saxe.

My tiny example convinced me that we want to reason in TLA, not in LP. To do this, we need to translate a TLA proof into the language of the theorem prover. The user should write the proof in the hierarchical style of [101], and the prover should check each step. One of the advantages of this approach turned out to be that it allows separate translations for the action reasoning and temporal reasoning. This is important because about 95% of a proof consists of action reasoning, and these proofs are much simpler if done with a special translation than in the same translation that handles temporal formulas. (In action reasoning, x and x’ are two completely separate variables; x’ is handled no differently than the variable y.) So, I invited Urban Engberg and Peter Grønning, who were then graduate students in Denmark, to SRC for a year to design and implement such a system. The result of that effort is described in this paper. For his doctoral research, Engberg later developed the system into one he called TLP.

Georges Gonthier demonstrated how successful this system was in his mechanical verification of the concurrent garbage collector developed by Damien Doligez and hand-proved in his thesis. Gonthier estimated that using TLP instead of working directly in LP reduced the amount of time it took him to do the proof by about a factor of five. His proof is reported in:

Georges Gonthier, Verifying the Safety of a Practical Concurrent Garbage Collector, in Rajeev Alur, Thomas A. Henzinger (Ed.): Computer Aided Verification, 8th International Conference, CAV ’96. Lecture Notes in Computer Science, Vol. 1102, Springer, 1996, 462-465.

TLP’s input language was essentially a very restricted subset of TLA+ (described in [127])–a language that did not exist when TLP was implemented. Extending it to handle all of TLA+ would be a simple matter of programming. However, TLP is no longer maintained and probably no longer works, since it was based on an old version of the LP prover. Moreover, LP no longer seems to be the best prover to use. The next step is an industrial-strength system that accepts all of TLA+ and that makes it easy to add different theorem provers as back ends, so the user can have a choice of what prover to use for each step. I am still waiting for someone to volunteer to build such a system.