Model Checking TLA
+ Specifications
Yuan Yu6 
, Panagiotis Manolios7 and Leslie Lamport6
| (6) |
Compaq Systems Research Center, USA |
| (7) |
Department of Computer Sciences, University of Texas at Austin, USA |
Abstract
TLA+ is a specification language for concurrent and reactive systems that combines the temporal logic TLA with full first-order
logic and ZF set theory. TLC is a new model checker for debugging a TLA+ specification by checking invariance properties of a finite-state model of the specification. It accepts a subclass of TLA+ specifications that should include most descriptions of real system designs. It has been used by engineers to find errors
in the cache coherence protocol for a new Compaq multiprocessor. We describe TLA+ specifications and their TLC models, how TLC works, and our experience using it.
Acknowledgments Homayoon Akhiani and Josh Scheid wrote the specification of the cache coherence protocol to which we are applying TLC. Mike
Burrows suggested that TLC be disk based and recommended the second method of using the disk. Damien Doligez and Mark Tuttle
are early users who provided valuable feedback. Sanjay Ghemawat implemented the high-performance Java runtime that we have
been using. Jean-Charles Gregoire wrote the TLA+ parser used by TLC. Mark Hayden is helping us improve the performance of
TLC. Allan Heydon advised us on performance pitfalls in Java class libraries.
References secured to subscribers.