Semantics driven dynamic partial-order reduction of MPI-based parallel programs

ABSTRACT

Most distributed parallel programs in the high performance computing (HPC) arena are written using the MPI library. There is growing interest in using model checking for debugging these MPI programs. In this context, partial-order reduction has considerable potential for containing state explosion, given the distributed memory nature of MPI programs. This potential is largely unmet. In this paper, we first define the formal semantics for a non-trivial subset of MPI. We then prove independence theorems based on theformal semantics, paving the way to a semantically clear and general partial-order reduction approach for MPI. Our work describes, for the first time, the exact dependencies between MPI non-blocking send operations and their tests for completion, namely wait and test. We also offer a cleaner solution than in previous works for MPI wildcard receives,a proper handling of which requires knowledge of the future course of computations. We show that Flanagan and Godefroid's dynamic patial-order reduction algorithm offers a natural way to handle the need for future information. Our initial experimental results are encouraging.

REFERENCES

• 1: T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: A model checker for concurrent software. In CAV 2004:16th International Conference on Computer Aided Verification, Boston, Massachusetts, July 2004, LNCS. Springer-Verlag, 2004.
• 2: Steven Barrus, Ganesh Gopalakrishnan, Robert M. Kirby, and Robert Palmer. Verification of MPI programs using SPIN. Technical Report UUCS-04-008, The University of Utah, 2004.
• 3: Twan Basten , Dragan Bošnački , Marc Geilen, Cluster-Based Partial-Order Reduction, Automated Software Engineering, v.11 n.4, p.365-402, October 2004 [doi>10.1023/B:AUSE.0000038937.18006.3d]
• 4: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 5: Jayant DeSouza , Bob Kuhn , Bronis R. de Supinski , Victor Samofalov , Sergey Zheltov , Stanislav Bratanov, Automated, scalable debugging of MPI programs with Intel® Message Checker, Proceedings of the second international workshop on Software engineering for high performance computing system applications, May 15-15, 2005, St. Louis, Missouri [doi>10.1145/1145319.1145342]
• 6: Cormac Flanagan , Patrice Godefroid, Dynamic partial-order reduction for model checking software, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.110-121, January 12-14, 2005, Long Beach, California, USA
• 7: Philippe Georgelin, Laurence Pierre, and Tin Nguyen. A formal specification of the MPI primitives and communication mechanisms. Technical report, LIM, 1999.
• 8: Patrice Godefroid , J. van Leeuwen , J. Hartmanis , G. Goos , Pierre Wolper, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 9: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 10: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 11: Rajit Manohar , Alain J. Martin, Slack Elasticity in Concurrent Computing, Proceedings of the Mathematics of Program Construction, p.272-285, June 15-17, 1998
• 12: MPI: A Message-Passing Interface Standard. http://www.mpi-forum.org/docs/mpi-11-html/mpi-report.html.
• 13: Robert Palmer, Steven Barrus, Yu Yang, Ganesh Gopalakrishnan, and Robert M. Kirby. Gauss: A framework for verifying scientific computing software. In SoftMC: Workshop on Software Model Checking, number 953 in ENTCS, August 2005.
• 14: Robert Palmer, Ganesh Gopalakrishnan, and Robert M. Kirby. The communication semantics of the message passing interface. Technical Report UUCS-06-012, The University of Utah, October 2006.
• 15: Robert Palmer, Ganesh Gopalakrishnan, and Robert M. Kirby. Semantics Driven Dynamic Partial-order Reduction of MPI-based Parallel Programs (full version). Technical Report UUCS-07-011, University of Utah, School of Computing, 2007.
• 16: Salman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp. Formal verification of programs that use mpi one-sided communication. In Recent Advances in Parallel Virtual Machine and Message Passing Interface, volume 4192/2006 of LNCS, pages 30{39, Berlin/Heidelberg, 2006. Springer.
• 17: http://research.microsoft.com/phoenix.
• 18: Robby , Matthew B. Dwyer , John Hatcliff, Bogor: an extensible and highly-modular software model checking framework, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 19: Stephen F. Siegel. Efficient verification of halting properties for mpi programs with wildcard receives. In Radhia Cousot, editor, Verification, Model Checking, and Abstract Interpretation: 6th International Conference, VMCAI 2005, pages 413{429, Paris, January 2005. Springer-Verlag.
• 20: Stephen F. Siegel. Model checking nonblocking mpi programs. In B. Cook and A. Podelski, editors, VMCAI 07, number 4349 in LNCS, pages 44{58. Springer-Verlag, 2007.
• 21: Stephen F. Siegel and George Avrunin. Analysis of mpi programs. Technical Report UM-CS-2003-036, Department of Computer Science, University of Massachusetts Amherst, 2003.
• 22: Stephen F. Siegel and George S. Avrunin. Verification of mpi-based software for scientific computation. In Proceedings of the 11th International SPIN Workshop on Model Checking Software, volume 2989 of LNCS, pages 286{303, Barcelona, April 2004. Springer.
• 23: Stephen F. Siegel , George S. Avrunin, Modeling wildcard-free MPI programs for verification, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065957]
• 24: Antti Valmari, A Stubborn Attack On State Explosion, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.156-165, June 18-21, 1990

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
          Subjects: Distributed programming
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

General Terms:
Verification

Keywords:
MPI, concurrent program semantics, model checking, partial-order reduction, transition independence