Parallelizing the Murϕ verifier

U Stern, DL Dill - Formal Methods in System Design, 2001 - Springer
Formal Methods in System Design, 2001Springer
With the use of state and memory reduction techniques in verification by explicit state
enumeration, runtime becomes a major limiting factor. We describe a parallel version of the
explicit state enumeration verifier Murϕ for distributed memory multiprocessors and
networks of workstations using the message passing paradigm. In experiments with three
complex cache coherence protocols on an Sp2 multiprocessor and on a network of
workstations at UC Berkeley, parallel Murϕ shows close to linear speedups, which are …
Abstract
With the use of state and memory reduction techniques in verification by explicit state enumeration, runtime becomes a major limiting factor. We describe a parallel version of the explicit state enumeration verifier Murϕ for distributed memory multiprocessors and networks of workstations using the message passing paradigm. In experiments with three complex cache coherence protocols on an Sp2 multiprocessor and on a network of workstations at UC Berkeley, parallel Murϕ shows close to linear speedups, which are largely insensitive to communication latency and bandwidth. There is some slowdown with increasing communication overhead, for which a simple yet relatively accurate approximation formula is given. Techniques to reduce overhead and required bandwidth and to allow heterogeneity and dynamically changing load in the parallel machine are discussed, which we expect will allow good speedups when using conventional networks of workstations.
Springer