The Wildfire Verification Challenge Problem
Last modified 28 May 2002
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.
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 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
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.
- Click here for a gzipped
Unix tar file. (1 MB)
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
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