(Aspnes & Herlihy)
Cadence SMV is a proof assistant which supports several compositional methods methods [McM98, McM99, MQS00]. These methods allow the verification of large, complex, systems by reducing the verification problem to small problems that can be solved automatically by model checking. Cadence SMV provides a variety of such techniques including induction, circular compositional reasoning, temporal case splitting and data type reduction.
There are two main challenges posed by the randomised consensus protocol of Aspnes and Herlihy [AH90]: firstly, the round numbers are unbounded, leading to an infinite data type NUM, and, secondly, we wish to prove the correctness of the protocol for any number of processes, or, in other words, for all values of N. We achieve this by suitably combining data type reduction (ordset) with induction, circular compositional reasoning and temporal case splitting.
Recall that we can verify the properties: Validity and Agreement and the non-probabilistic arguments of Probabilistic wait-free termination using conventional model checking methods, by replaced the probabilistic choices with nondeterministic ones.
The Cadence SMV description of the randomised consensus protocol of [AH90], with the probabilistic choices with nondeterministic choices, can be found here (also as a pdf file here).
We are grateful to Ken McMillan for supplying a recent version of Cadence SMV and suggesting appropriate proof methods. Note that the version of Cadence SMV we have used is not fully compatible with the release of 08.08.00.
The proof of validity can be found here (also as a pdf file here) and the output from Cadence SMV here.
Agreement is the most difficult of the requirements to prove. The main step of proving agreement is proving Invariant 6.3 of [PSL00]. To simplify the proof and to keep the model checking feasible we had split the proof up into separate parts: assuming the properties proved in one while proving the others. The complete proof of Invariant 6.3 can be found here (also as a pdf file here) and the output from Cadence SMV here.
The proof agreement (which assumes Invariant 6.3) can be found here (also as a pdf file here) and the output from Cadence SMV here.
To prove agreement we additionally needed to prove that Lemma 6.12 of [PSL00] holds, the proof of which can be found here here (also as a pdf file here) and the output from Cadence SMV here.
The proof of the non-probabilistic aguments in the proof of probabilistic wait-free termination can be found here (also as a pdf file here) and the output from Cadence SMV here.
In all the above proofs certain invariants are assumed. The proof of these additional invariants can be found here (also as a pdf file here) and the output from Cadence SMV here.