Certain protocols are designed to simulate a sequence of atomic transactions. However, because the implementation is distributed, it breaks up each transaction into a sequence of smaller steps. The steps of a single transaction may be executed by different nodes of the distributed system. We have developed a general method, which we call aggregation, for using an automated theorem-prover to verify such transaction-oriented protocols. This work has primarily been applied to multiprocessor cache coherence protocols.
The aggregation method verifies a description of a protocol implementation by comparing it with a specification. The specification is an idealized description of a protocol where all transactions are atomic (the transactions are executed instantaneously). The implementation implements each transaction in a series of steps which may be executed at a variety of processing sites (nodes), which communicate by sending messages over a network of some kind.
The aggregation method requires understanding how a sequence of implementation steps implements a transactions. The sequence must have a commit point, where the transaction is irrevocable. Usually, the commit point is the first point at which there is a visible state change from the transaction. After the commit point of a transaction has occured, there are usually additional steps that need to occur to complete the transaction.
As in our approach to processor verification, the aggregation method requires the user to define an abstraction function, which maps implementation states to specification states. The key point in the aggregation method is how this function is defined: the aggregation function must complete all transactions that have been committed but have not yet completed. Once the transaction is completed, the aggregation function projects away parts of the implementation state that do not appear in the specification (e.g., the network). The idea of completing unfinished transactions is a similar to (and was inspired by) the concept of flushing in our processor verification work.
Most of our work on aggregation has been done in the context of the PVS theorem-prover from SRI's Computer Science Laboratory. The implementation and specification are described as a collection of next-state rules (similar in style to Murphi) using the PVS language, and the aggregation function was described in the PVS language directly. We have verified several interesting examples, including a distributed list protocol (which is part of a directory-based cache coherence protocol) and a majority concensus algorithm for distributed multiple-copy databases. However, the most impressive example we have done so far is a proof of correctness of the cache coherence protocol for the Stanford FLASH multiprocessor. We have also verified one real-life industrial cache coherence protocol, which turned out to be simpler than FLASH (sorry, we can't discuss this example in more detail yet).
The basic theory of verification using aggregation is described in the following conference paper:
[PD96A] Seungjoon Park and David L. Dill. "Protocol Verification by Aggregation of Distributed Transactions," International Conference on Computer-Aided Verification, pp. 300-310, LNCS 1102, July 1996.
The verification of the cache coherence protocol for FLASH is described in another conference paper:
[PD96B] Seungjoon Park and David L. Dill. "Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions," 8th ACM Symposium on Parallel Algorithms and Architectures, pp. 288-296, June 1996.
A journal paper combining some results from the two previous papers, along with a soundness theorem should appear soon:
[PD98] Seungjoon Park and David L. Dill. "Verification of Cache Coherence Protocols By Aggregation of Distributed Transactions." To appear in Mathematical Systems Theory.
More details of the theory and examples are available in Seungjoon Park's PhD thesis:
[ParkThesis] Seungjoon Park. "Computer Assisted Analysis of Multiprocessor Memory Systems," Ph.D. Thesis, Computer Systems Laboratory Technical Report CSL-TR-96-696, Stanford University, June 1996.
Thereom provers are usually better at proving things correct than at finding and diagnosing errors. Therefore, it is very useful to be able to do initial "sanity checking" on a verification example using a finite-state verifier such as Murphi. This requires "scaling down" the example, so that it has a small number of finite-state processes. Murphi is best at checking simple invariants; the only problem was that we did not know how to use Murphi to check aggregation proofs. Recently, we proposed an efficient technique for checking aggregation abstractions automatically using Murphi.
The following paper shows how to convert an aggregation verification problem to simple invariants, so it can be check using Murphi:
[PDD97] Seungjoon Park, Satyaki Das, and David L. Dill. "Automatic Checking of Aggregation Abstractions Through State Enumeration," IFIP TC6/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, November 1997.