The Avalanche effort will involve the development of numerous concurrent protocols implemented both in software and in hardware. We realize the importance of verifying these protocols using systematic methods so that our experimental studies of the Avalanche multiprocessor are not hampered by frequent system crashes. Protocol verification will be conducted using two approaches: (1) the conventional method in which a battery of tests will be applied to the simulation model; and (2) formal verification techniques that will allow us to establish safety and liveness properties with respect to the verification model. To minimize the effort in obtaining the verification model from the simulation model, we will use a verification-oriented language called Promela that is close to conventional programming languages. The Promela verifier, SPIN, is one of the most widely distributed finite-state protocol verifier in use today.
We have evaluated Promela and SPIN using several examples that typify what will be actually encountered in Avalanche. Additional insight was obtained by a student member of the Avalanche group, Ratan Nalumasu, who did a summer internship under Drs. Robert Kurshan and Gerard Holzmann, the developers of Promela at AT&T Bell Labs. Our initial experience indications that the formal verification framework offered by Promela and SPIN is easy to learn and natural to use by members of the Avalanche team. In addition, critical protocols expressed directly in real-world languages such as C or VHDL can be (with some effort) translated into Promela for verification. In addition, we have noticed some limitations of SPIN, the main one being that of state explosion in handling systems with identical replicated components (as in multiprocessor networks, cache directories, etc.) Our efforts to combat this state explosion are summarized in the following subsection.
We have studied existing methods for combating state explosion in finite-state verification. Most of these techniques are either too specialized or cannot handle all cases of symmetry that arise in real concurrent systems. To overcome these problems, a simple technique called state normalization was investigated. State normalization attempts to "sort" system state-vectors generated during finite-state verification so that most redundant cases are eliminated from consideration. State normalization has worked well for the practical examples we have tried; more studies are underway. An open issue at this point was the kind of safety and liveness properties preserved by normalization.
We have discovered that state normalization preserves all safety properties and, in addition, algorithms for checking for liveness under weak-fairness can be easily incorporated into SPIN. Currently we have come up with one version of this latter algorithm, and are in the process of incorporating it into SPIN. Our ongoing work is geared towards making Promela and SPIN efficient-enough to handle verification situations that will arise during the Avalanche effort, by investigating techniques such as state normalization, and several others.
We are also in the process of improving our ties with key players in the verification community, notably the AT&T group consisting of Drs. Kurshan and Holzmann, and Professor David Dill of Stanford. In this connection, Nalumasu will spend another two months at AT&T and Ganesh Gopalakrishnan, an Avalanche faculty associate, will spend part of his upcoming sabbatical at Stanford working with Prof. Dill and his group.
This work was sponsored by the
Space and Naval Warfare Systems Command (SPAWAR) and
Advanced Research Projects Agency (ARPA),
Communication and Memory Architectures for
Scalable Parallel Computing,
ARPA order #B990 under SPAWAR contract #N00039-95-C-0018
Back to the
Avalanche Project Home Page,
or Computer Science Department Home Page.
Feedback to <avalanche@jensen.cs.utah.edu>.