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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
S. Aggarwal, R. Alonso, and C. Courcoubetis, “Distributed reachability analysis for protocol verification environments,” in Discrete Event Systems: Models and Applications, IIASA Conference, 1987, pp. 40–56.
A. Alexandrov, M.F. Ionescu, K.E. Schauser, and C. Scheiman, “LogGP: Incorporating long messages into the LogP model—one step closer towards a realistic model for parallel computation,” in 7th Annual ACM Symposium on Parallel Algorithms and Architectures, 1995, pp. 95–105.
J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill, “Sequential circuit verification using symbolic model checking,” in 27th ACM/IEEE Design Automation Conference, 1990, pp. 46–51.
J.L. Carter and M.N. Wegman, “Universal classes of hash functions,” Journal of Computer and System Sciences,” Vol. 18, No. 2, 143–154, 1979.
D. Culler, R. Karp, D. Patterson, A. Sahay, K.E. Schauser, E. Santos, R. Subramonian, and T. von Eicken, “LogP: Towards a realistic model of parallel computation,” in 4th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 1993, pp. 1–12.
D. Culler, K. Keeton, C. Krumbein, L.T. Liu, A. Mainwaring, R. Martin, S. Rodrigues, K. Wright, and C. Yoshikawa, Generic Active Message Interface Specification, UC Berkeley, 1995. Version 1.1 http:// now.cs.berkeley.edu/papers2/.
D.L. Dill, “The Mur' verification system,” in Computer Aided Verification, 8th International Conference, 1996, pp. 390–393.
W. Feller, An Introduction to Probability Theory and Its Applications, vol. 1, John Wiley & Sons, New York, 3rd ed. 1968.
G.J. Holzmann, “On limits and possibilities of automated protocol analysis,” in Protocol Specification, Testing, and Verification, 7th International Conference, 1987. pp. 339–344.
G.J. Holzmann and D. Peled, “The state of SPIN,” in Computer Aided Verification, 8th International Conference, 1996, pp. 385–389.
A.J. Hu, “Techniques for efficient formal verification using binary decision diagrams,” PhD thesis, Stanford University, 1995.
IEEE Std 1596-1992, IEEE Standard for Scalable Coherent Interface (SCI).
C.N. Ip, “State reduction methods for automatic formal verification,” PhD thesis, Stanford University, 1996.
S. Kimura and E.M. Clarke, “A parallel algorithm for constructing binary decision diagrams,” in IEEE International Conference on Computer Design, 1990, pp. 220–223.
N. Kumar and R. Vemuri, “Finite state machine verification on MIMD machines,” in European Design Automation Conference, 1992, pp. 514–520.
J. Kuskin, D. Ofelt, M. Heinrich, J. Heinlein, R. Simoni, K. Gharachorloo, J. Chapin, D. Nakahira, J. Baxter, M. Horowitz, A. Gupta, M. Rosenblum, and J. Hennessy, “The Stanford FLASH multiprocessor,” in 21st Annual International Symposium on Computer Architecture, 1994, pp. 302–313.
D. Lenoski, J. Laudon, K. Gharachorloo, W.-D. Weber, A. Gupta, J. Hennessy, M. Horowitz, and M.S. Lam, “The Stanford DASH multiprocessor. Computer,” Vol. 25 No. 3, pp. 63–79, 1992.
R.P. Martin, A.M. Vahdat, D.E. Culler, and T.E. Anderson, “Effects of communication latency, overhead, and band width in a cluster architecture,” in 24th Annual International Symposium on Computer Architecture, 1997.
R.K. Ranjan, J.V. Sanghavi, R.K. Brayton, and A. Sangiovanni-Vincentelli, “Binary decision diagrams on network of workstations,” in International Conference on Computer Design, 1996, pp. 358–364.
U. Stern, “Algorithmic techniques in verification by explicit state enumeration,” PhD thesis, Technical University of Munich, 1997.
U. Stern and D.L. Dill, Using magnetic disk instead of main memory in the Murϕ verifier, Computer Aided Verification, 10th International Conference, 1998, pp. 172–183.
U. Stern and D.L. Dill, “A new scheme for memory-efficient probabilistic verification,” in Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, 1996, pp. 333–348.
U. Stern and D.L. Dill, “Parallelizing the Murϕ verifier,” in Computer Aided Verification, 9th International Conference, 1997, pp. 256–267.
T. Stornetta, “Implementation of an efficient parallel BDD package,” Master's thesis, UC Santa Barbara, 1995.
T. Stornetta and F. Brewer, “Implementation of an efficient parallel BDD package,” in 33rd Design Automation Conference, 1996, pp. 641–644.
T. von Eicken, D.E. Culler, S.C. Goldstein, and K.E. Schauser, “Active messages: A mechanism for integrated communication and computation,” in 19th Annual International Symposium on Computer Architecture, 1992, pp. 256–266.
C.-P. Wen, A distributed task queue for load balancing on the CM5. Unpublished paper written in Katherine Yelick's group at UC Berkeley.
P. Wolper and D. Leroy, “Reliable hashing without collision detection,” in Computer Aided Verification. 5th International Conference, 1993, pp. 59–70.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Stern, U., Dill, D.L. Parallelizing the Murϕ Verifier. Formal Methods in System Design 18, 117–129 (2001). https://doi.org/10.1023/A:1008771324652
Issue Date:
DOI: https://doi.org/10.1023/A:1008771324652