Further cache coherence protocols

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 [4] ).

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)