The Wildfire Challenge Problem

Abstract

We pose as a challenge to the verification community the problem of finding errors in the specification of a complicated cache-coherence protocol. It specifies a simplified version of the protocol used in an actual multiprocessor computer, except with one error deliberately introduced and another introduced by accident. The protocol and the memory model it is supposed to implement are described here; their complete specifications are posted on the Web. Contents 1