Cache protocols play a key role in the modern parallel or distributed computer systems. They are complex algorithms that must deal with asynchrony, unpredictable message delays, and multiple paths between many processes. Due to high concurrency, a system consisting of only 4-5 nodes, which runs cache protocol, has a huge number of possible executions, let alone the practical systems consisting of hundred of nodes. So neither unaided human reasoning nor traditional simulation-based validation can be relied upon to flush out all bugs. On the other side, formal methods are mathematically based techniques for specifying and verifying systems. Their mathematical underpinning allows formal methods to exhaustive state space exploration, and this can produce a high degree of confidence in the correctness of a cache protocol.
Mechanical theorem proving and model checking are the two main methods applied to formal verification for cache protocols, each with its strength and weakness. Mechanical theorem proving is more general, and makes available the full power of formal mathematics and logic, to deal with the infinite states. The lemmas and proofs so obtained exactly show the invariants of the verified protocols and why the invariants hold. However, mechanical theorem proving requires human guidance to some theorem prover. Users need complete knowledge of both the protocols verified and the theorem-prover used. Model-checking enumerates all the reachable states of the protocol, checking whether the specified properties are satisfied. It is fully automatic, but is applicable to only the verification of a small system, and suffers from state exploration problem when the size of the verified system is large. Typically, the configuration size is 3 or 4. Model-checking can not answer why the protocol is correct in any system which consists of arbitrary number of nodes.
We want combine model-checking and theorem proving to verify the invariants of cache protocol. Recently, Chou, Mannava, and Park [A Simple Method for Parameterized Verification of Cache Coherence Protocols, FMCAD 2004: 382-398] proposes an iterative "counter-example-guided abstraction refinement" principle to construct an abstract model. Roughly speaking, they start from a naïve model, then refine it by the aforementioned principle. At each step, the analysis of the counterexample trace provided by the model checker results in: (a) locating a rule of the building model that causes the counterexample; (b) finding a new purported invariant which can be used to strengthen the guard so that the offending transitions becomes impossible. This process is completed when the invariants considered and all newly added invariants can be satisfied in the abstraction model.
Unfortunately the mathematical foundation of their work is by no means so simple as regarded. Their accountings are too sketchy, and not easy to be understood. It is necessary to formalise the mathematical foundation in a formal theorem prover, which can help us to achieve the highest possible assurance for all the results.
We redo their refinement experiments by using Spin to construct the
abstract model, furthermore, we propose a semantics basing on traces, and
formally prove why the abstract model can account for the correctness of a
German protocol instance with an arbitrary size. We formalize our theory in
Isabelle/HOL.
Our work is listed as follows.
A. German protocol with size 3.
B. German_err1 protocol with size 3
C. German_cherr protocol with size 3
E. The proof
of the mathematical foundation of the refinement approach
Some notes:
1. Each of the zip file of A-D contains two files, one file is the original Murphi file, the other is our Spin file.
2. German_err1, and German_cherr are two protocol with errors, which are deliberately set by Steven German.
A paper has been prepared for submission:
The
Mathematical Foundations of Guard strengthening and Parameter Abstraction