Model Checking Nonblocking MPI Programs

  • Stephen F. Siegel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4349)


This paper explores a way to apply model checking techniques to parallel programs that use the nonblocking primitives of the Message Passing Interface (MPI). The method has been implemented as an extension to the model checker Spin called Mpi-Spin. It has been applied to 17 examples from a widely-used textbook on MPI. Many correctness properties of these examples were verified and in two cases nontrivial faults were discovered.


Model Check Local Memory Message Passing Interface Message Passing Interface Process Promela Model 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Holzmann, G.J.: The Spin Model Checker. Addison-Wesley, Boston (2004)Google Scholar
  2. 2.
    Matlin, O.S., Lusk, E., McCune, W.: SPINning parallel systems software. In: Bošnački, D., Leue, S. (eds.) Model Checking Software. LNCS, vol. 2318, pp. 11–13. Springer, Heidelberg (2002)Google Scholar
  3. 3.
    Message Passing Interface Forum: MPI: A Message-Passing Interface standard, version 1.1, (1995)
  4. 4.
    Message Passing Interface Forum: MPI-2: Extensions to the Message-Passing Interface. (1997)
  5. 5.
    Pervez, S., et al.: Formal verification of programs that use MPI one-sided communication. In: Mohr, B., et al. (eds.) Recent Advances in Parallel Virtual Machine and Message Passing Interface. LNCS, vol. 4192, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Post, D.E., Votta, L.G.: Computational science demands a new paradigm. Physics Today, 35–41 (January 2005)Google Scholar
  7. 7.
    Siegel, S.F.: Efficient verification of halting properties for MPI programs with wildcard receives. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 17–19. Springer, Heidelberg (2005)Google Scholar
  8. 8.
    Siegel, S.F., Avrunin, G.S.: Modeling MPI programs for verification. Technical Report UM-CS-2004-75, Department of Computer Science, University of Massachusetts (2004)Google Scholar
  9. 9.
    Siegel, S.F., Avrunin, G.S.: Verification of MPI-based software for scientific computation. In: Graf, S., Mounier, L. (eds.) Model Checking Software. LNCS, vol. 2989, pp. 1–3. Springer, Heidelberg (2004)Google Scholar
  10. 10.
    Siegel, S.F., Avrunin, G.S.: Modeling wildcard-free MPI programs for verification. In: Proceedings of the 2005 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. PPoPP’05, Chicago, Illinois, USA, June 15–17, 2005, pp. 15–17. ACM Press, New York (2005)Google Scholar
  11. 11.
    Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: Pollock, L., Pezzé, M.(eds.). ISSTA 2006: Proceedings of the ACM SIGSOFT 2006 International Symposium on Software Testing and Analysis, Portland, ME, pp. 157–168 (2006)Google Scholar
  12. 12.
    Snir, M., Otto, S., Huss-Lederman, S., Walker, D., Dongarra, J.: MPI—The Complete Reference, Volume 1: The MPI Core. MIT Press, second edition (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Stephen F. Siegel
    • 1
  1. 1.Department of Computer and Information Sciences, University of Delaware, Newark, DE 19716USA

Personalised recommendations