The Wildfire Verification Challenge Problem

Last modified 28 May 2002

The Challenge

We have written formal specifications of a cache-coherence protocol and its correctness condition.  The protocol's specification contains a bug.  The challenge problem is to find the bug.

Wildfire

The challenge problem's cache-coherence protocol is a simplified version of the protocol for an Alpha multiprocessor, code-named Wildfire, into which we have inserted a bug.  Its correctness condition is a simplified version of the Alpha memory model. 

Wildfire is a system of processors connected in a hierarchical network.  It has the most complicated cache-coherence protocol we know of.  The challenge problem uses a greatly simplified version of that protocol, but it is still fairly complicated. The bug was inserted by us; to our knowledge, it was never present in the actual system design.  We think that trying to find it poses a practical test of the efficacy of a verification method.

The Specifications

The protocol and its correctness condition are specified in TLA+, a formal language based on the Temporal Logic of Actions (TLA).  The specifications consist of about 900 lines of TLA+, exclusive of comments.  The specifications are extensively commented, and additional material explaining TLA+ is included.  We do not expect computer scientists to have much difficulty understanding the meaning of the specifications, even if they are unfamiliar with TLA.

Downloading the Problem

The specifications and related material--including papers describing TLA--are contained in a collection of files.  The README file explains what is in the other files.  The files are available here:
Click here for a zip file.  (1 MB)
Click here for a Unix tar file.  (2 MB)
Click here for a gzipped Unix tar file.  (1 MB)
Note: Obsolete versions of standard modules were removed from these files on 14 April 2020.

The Rules

If you find the bug or have a question about the problem, please send email to Leslie Lamport. Please do not post any solution without first checking with us.  We recommend that you contact us if you intend to work on the problem, so we can notify you of any corrections or clarifications.  We also suggest that you keep track of how much time you spend on the problem.

The First Solution

 On 2 August 2000, Georges Gonthier reported that he had found two bugs.  One is the bug that we had inserted into the protocol.  The other is a relatively simple error resulting from an oversight on our part.  He found both errors without any mechanical assistance.  The presence of a second error should make the challenge problem more fun, so we will not reveal it.

This problem is being posed by Leslie Lamport, Mark Tuttle, and Yuan Yu.  We were helped by the designers of the system on which it is based, Kourosh Gharachorloo, Madhu Sharma, Simon Steely, and Steve van Doren, and by Paul Harter.


This page can be found by searching the Web for the 24-letter string wildfirechallengeproblem. Please do not put this string in any document that could wind up on the web--including email messages and Postscript and Word documents.  One way to refer to it in Web documents is as "the string obtained by removing the two - characters from wildfi-rechall-engeproblem".