Along with Amy Felty and Frank Stomp at Bell Labs, Howe has been using
Nuprl to verify the portion related to cache coherence of the SCI
(Scalable Coherent Interface) protocol [18]. This
protocol is an IEEE standard for specifying communication between
shared memory multiprocessors, and is called scalable because it is
intended for systems which may consist of up to 64,000 processors. An
attempt to validate the program verified in the current paper has been
made by the model checking community. Holzmann using SPIN
[13], Kurshan using COSPAN [20], and Long and
McMillan using SMV [22] report to have validated the
program for up to five processes (at which point the state explosion
problem takes its toll). Stern and Dill [33] have
encountered similar state-explosion problems using Mur
, though
they were nevertheless able to find several errors in the C-code for
the protocol.
The reason this particular protocol was chosen for a verification project was because of its complexity, because of its general similarity to communication protocols of interest to Lucent, and also because of local expertise. The current Nuprl effort directly formalizes the proof described in the paper [9], and does not involved any external tools. We plan to test the LPE by redoing the verification, but using model-checkers to speed up the process, for example by verifying some of the properties using formally justified abstractions. The connection to model checkers could be direct, or could be imported from, e.g., HOL or PVS, via the planned sound link with these systems.