TLA+ Verification of Cache-Coherence Protocols

Mark Tuttle, Yuan Yu, and I formed a small group applying TLA to verification problems at Compaq. Our two major projects, in which we have had other collaborators, have been verifications of protocols for two multiprocessor Alpha architectures. We thought it would be a good idea to write a paper describing our experience doing verification in industry. The FM’99 conference had an Industrial Applications track, to include “Experience reports [that] might describe a case study or industrial project where a formal method was applied in practice.” So, we wrote this paper and submitted it. It was rejected. One of the referees wrote, “The paper is rather an experience report than a scientific paper.” Our paper is indeed short on details, since neither system had been released at that time and almost all information about it was still company confidential. However, I think it still is worth reading if you’re interested in what goes on in the industrial world.