Up: Verification via Supercompilation
Previous: Verification of MESI cache
We have applied our approach and successfully verified all parameterised cache coherence protocols
taken from [4,5]
(see also related web page Automatic Verification of Parameterized Synchronous Systems).
In what follows we present a Refal
encoding of a protocol, result of
supercompilation and time it has taken.
The time is evaluated very roughly, for our
first goal was to check a feasibility of an approach, not a precise timing. One indication that our approach
is quite efficient is that the verification of Futurebus+ protocol has taken around 3 seconds
(compare with around 3 min reported (in the year 2000, though) for the verification of the same protocol,
In all cases the correctness of protocols follows from the fact that the result
of supercompilation does
not contain an experession False (see section 4 for explanations)