Formal verification of practical MPI programs

ABSTRACT

This paper considers the problem of formal verification of MPI programs operating under a fixed test harness for safety properties without building verification models. In our approach, we directly model-check the MPI/C source code, executing its interleavings with the help of a verification scheduler. Unfortunately, the total feasible number of interleavings is exponential, and impractical to examine even for our modest goals. Our earlier publications formalized and implemented a partial order reduction approach that avoided exploring equivalent interleavings, and presented a verification tool called ISP. This paper presents algorithmic and engineering innovations to ISP, including the use of OpenMP parallelization, that now enables it to handle practical MPI programs, including:(i)~ParMETIS - a widely used hypergraph partitioner, and (ii)~MADRE - a Memory Aware Data Re-distribution Engine, both developed outside our group. Over these benchmarks, ISP has automatically verified up to 14K lines of MPI/C code, producing error traces of deadlocks and assertion violations within seconds.

REFERENCES

• 1: http://www.cs.utah.edu/formal_verification/ISP
• 2: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 3: 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
• 4: Al Geist, Sustained Petascale: The Next MPI Challenge, Proceedings of the 14th European PVM/MPI User's Group Meeting on Recent Advances in Parallel Virtual Machine and Message Passing Interface, September 30-October 03, 2007, Paris, France [doi>10.1007/978-3-540-75416-9_2]
• 5: P. Godefroid.Partial-Order Methods for the Verification of Concurrent Systems: An approach to the State-Explosion Problem. PhD thesis, Universite De Liege, 1994--95.
• 6: P. Godefroid, B. Hanmer, and L. Jagadeesan. Systematic software testing using VeriSoft: An analysis of the 4ess heart-beat monitor. Bell Labs Technical Journal, 3(2), April-June 1998.
• 7: William Gropp , Ewing Lusk , Nathan Doss , Anthony Skjellum, A high-performance, portable implementation of the MPI message passing interface standard, Parallel Computing, v.22 n.6, p.789-828, Sept. 1996 [doi>10.1016/0167-8191(96)00024-5]
• 8: G. Karypis. METIS and ParMETIS. http://glaros.dtc.umn.edu/gkhome/views/metis.
• 9: George Karypis , Vipin Kumar, Parallel multilevel k-way partitioning scheme for irregular graphs, Proceedings of the 1996 ACM/IEEE conference on Supercomputing (CDROM), p.35-es, January 01-01, 1996, Pittsburgh, Pennsylvania, United States [doi>10.1145/369028.369103]
• 10: B. Krammer, K. Bidmon, M. S. Müller, and M. M. Resch. Marmot: An MPI analysis and checking tool. In Parallel Computing 2003, Sept. 2003.
• 11: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 12: Proceedings of the 15th European PVM/MPI Users' Group Meeting on Recent Advances in Parallel Virtual Machine and Message Passing Interface, September 2008
• 13: G. Luecke, H. Chen, J. Coyle, J. Hoekstra, M. Kraeva, and Y. Zou. MPI-CHECK: A tool for checking Fortran 90 MPI programs. Concurrency and Computation: Practice and Experience, 15:93--100, 2003.
• 14: Madanlal Musuvathi , Shaz Qadeer, Fair stateless model checking, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 15: V. Prasad. Scalable and Accurate Approaches to Program Dependence Analysis, Slicing, and Verification of Concurrent Object Oriented Programs. PhD thesis, Kansas State University, 2006.
• 16: Subodh Sharma , Sarvani Vakkalanka , Ganesh Gopalakrishnan , Robert M. Kirby , Rajeev Thakur , William Gropp, A Formal Approach to Detect Functionally Irrelevant Barriers in MPI Programs, Proceedings of the 15th European PVM/MPI Users' Group Meeting on Recent Advances in Parallel Virtual Machine and Message Passing Interface, September 07-10, 2008, Dublin, Ireland [doi>10.1007/978-3-540-87475-1_36]
• 17: S. V. Sharma, G. Gopalakrishnan, and R. M. Kirby. A survey of MPI related debuggers and tools. Technical Report UUCS-07-015, University of Utah, School of Computing, 2007. http://www.cs.utah.edu/research/techreports.shtml.
• 18: S. Siegel. The MADRE manual. http://vsl.cis.udel.edu/madre/.
• 19: S. F. Siegel and G. S. Avrunin. Verification of MPI-based software for scientific computation. In Proceedings of the 11th International SPIN Workshop on Model Checking Software, pages 286--303, 2004.
• 20: Stephen F. Siegel , Louis F. Rossi, Analyzing BlobFlow: A Case Study Using Model Checking to Verify Parallel Scientific Software, Proceedings of the 15th European PVM/MPI Users' Group Meeting on Recent Advances in Parallel Virtual Machine and Message Passing Interface, September 07-10, 2008, Dublin, Ireland [doi>10.1007/978-3-540-87475-1_37]
• 21: Stephen F. Siegel , Andrew R. Siegel, MADRE: The Memory-Aware Data Redistribution Engine, Proceedings of the 15th European PVM/MPI Users' Group Meeting on Recent Advances in Parallel Virtual Machine and Message Passing Interface, September 07-10, 2008, Dublin, Ireland [doi>10.1007/978-3-540-87475-1_31]
• 22: S. Vakkalanka, M. DeLisi, G. Gopalakrishnan, and R. M. Kirby. Scheduling considerations for building dynamic verification tools for MPI. In Parallel and Distributed Systems -- Testing and Debugging (PADTAD-VI), July 2008.
• 23: Sarvani Vakkalanka , Michael Delisi , Ganesh Gopalakrishnan , Robert M. Kirby , Rajeev Thakur , William Gropp, Implementing Efficient Dynamic Formal Verification Methods for MPI Programs, Proceedings of the 15th European PVM/MPI Users' Group Meeting on Recent Advances in Parallel Virtual Machine and Message Passing Interface, September 07-10, 2008, Dublin, Ireland [doi>10.1007/978-3-540-87475-1_34]
• 24: Sarvani Vakkalanka , Ganesh Gopalakrishnan , Robert M. Kirby, Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_9]
• 25: Jeffrey S. Vetter , Bronis R. de Supinski, Dynamic software testing of MPI applications with umpire, Proceedings of the 2000 ACM/IEEE conference on Supercomputing (CDROM), p.51-es, November 04-10, 2000, Dallas, Texas, United States
• 26: Y. Yang, X. Chen, G. Gopalakrishnan, and R. M. Kirby. Distributed dynamic partial order reduction based verification of threaded software. In SPIN, Lecture Notes in Computer Science, pages 58--75. Springer, 2007.
• 27: Yu Yang , Xiaofang Chen , Ganesh Gopalakrishnan , Robert M. Kirby, Efficient Stateful Dynamic Partial Order Reduction, Proceedings of the 15th international workshop on Model Checking Software, August 10-12, 2008, Los Angeles, CA, USA [doi>10.1007/978-3-540-85114-1_20]

INDEX TERMS

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

General Terms:
Verification

Keywords:
distributed programming, dynamic partial order reduction, message passing interface, model checking, mpi