Advertisement

Parallelizing the Murϕ verifier

  • Ulrich Stern
  • David L. Dill
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)

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 that is based on the message passing paradigm. In experiments with three complex cache coherence protocols, 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.

Keywords

Hash Function Parallel Machine Linear Speedup Binary Decision Diagram Reachability Analysis 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    S. Aggarwal, R. Alonso, and C. Courcoubetis. Distributed reachability analysis for protocol verification environments. In Discrete Event Systems: Models and Applications. IIASA Conference, pages 40–56, 1987.Google Scholar
  2. 2.
    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, pages 95–105, 1995.Google Scholar
  3. 3.
    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, pages 46–51, 1990.Google Scholar
  4. 4.
    J. L. Carter and M. N. Wegman. Universal classes of hash functions. Journal of Computer and System Sciences, 18(2):143–54, 1979.Google Scholar
  5. 5.
    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, pages 1–12, 1993.Google Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    D. L. Dill. The Murϕ verification system. In Computer Aided Verification. 8th International Conference, pages 390–3, 1996.Google Scholar
  8. 8.
    W. Feller. An Introduction to Probability Theory and Its Applications, volume 1. John Wiley & Sons, 3rd edition, 1968.Google Scholar
  9. 9.
    G. J. Holzmann. On limits and possibilities of automated protocol analysis. In Protocol Specification, Testing, and Verification. 7th International Conference, pages 339–44, 1987.Google Scholar
  10. 10.
    G. J. Holzmann and D. Peled. The state of SPIN. In Computer Aided Verification. 8th International Conference, pages 385–9, 1996.Google Scholar
  11. 11.
    A. J. Hu, G. York, and D. L. Dill. New techniques for efficient verification with implicitly conjoined BDDs. In 31st Design Automation Conference, pages 276–82, 1994.Google Scholar
  12. 12.
    IEEE Std 1596–1992, IEEE Standard for Scalable Coherent Interface (SCI).Google Scholar
  13. 13.
    C. N. Ip. State Reduction Methods for Automatic Formal Verification. PhD thesis, Stanford University, 1996.Google Scholar
  14. 14.
    S. Kimura and E. M. Clarke. A parallel algorithm for constructing binary decision diagrams. In IEEE International Conference on Computer Design, pages 220–3, 1990.Google Scholar
  15. 15.
    N. Kumar and R. Vemuri. Finite state machine verification on MIMD machines. In European Design Automation Conference, pages 514–20, 1992.Google Scholar
  16. 16.
    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, pages 302–13, 1994.Google Scholar
  17. 17.
    D. Lenoski, J. Laudon, K. Gharachorloo, W.-D. Weber, A. Gupta, J. Hennessy, M. Horowitz, and M. S. Lam. The Stanford DASH multiprocessor. Computer, 25(3):63–79, 1992.Google Scholar
  18. 18.
    R. P. Martin, A. M. Vahdat, D. E. Culler, and T. E. Anderson. Effects of communication latency, overhead, and bandwidth in a cluster architecture. In 24th Annual International Symposium on Computer Architecture, 1997.Google Scholar
  19. 19.
    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, pages 358–64, 1996.Google Scholar
  20. 20.
    U. Stern and D. L. Dill. Improved probabilistic verification by hash compaction. In Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pages 206–24, 1995.Google Scholar
  21. 21.
    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, pages 333–48, 1996.Google Scholar
  22. 22.
    T. Stornetta. Implementation of an efficient parallel BDD package. Master's thesis, UC Santa Barbara, 1995.Google Scholar
  23. 23.
    T. Stornetta and F. Brewer. Implementation of an efficient parallel BDD package. In 33rd Design Automation Conference, pages 641–4, 1996.Google Scholar
  24. 24.
    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, pages 256–66, 1992.Google Scholar
  25. 25.
    C.-P. Wen. A distributed task queue for load balancing on the CM5. Unpublished paper written in Katherine Yelick's group at UC Berkeley.Google Scholar
  26. 26.
    P. Wolper and D. Leroy. Reliable hashing without collision detection. In Computer Aided Verification. 5th International Conference, pages 59–70, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Ulrich Stern
    • 1
  • David L. Dill
    • 1
  1. 1.Department of Computer ScienceStanford UniversityStanford

Personalised recommendations