research-article

Formal verification of practical MPI programs

Authors:

Sarvani Vakkalanka,

Michael DeLisi,

Ganesh Gopalakrishnan,

Robert M. Kirby,

Rajeev ThakurAuthors Info & Claims

ACM SIGPLAN Notices, Volume 44, Issue 4

Pages 261 - 270

https://doi.org/10.1145/1594835.1504214

Published: 14 February 2009 Publication History

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]

E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Dec. 1999.

Digital Library

[3]

C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In POPL, pages 110--121. ACM, 2005.

Digital Library

[4]

A. Geist. Sustained Petascale: The next MPI challenge. Invited Talk at EuroPVM/MPI 2007.

Digital Library

[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]

W. Gropp, E. Lusk, N. Doss, and A. Skjellum. A high-performance, portable implementation of the MPI message passing interface standard. Parallel Computing, 22(6):789--828, Sept. 1996.

Digital Library

[8]

G. Karypis. METIS and ParMETIS. http://glaros.dtc.umn.edu/gkhome/views/metis.

[9]

G. Karypis and V. Kumar. Parallel multilevel k-way partitioning scheme for irregular graphs. In SuperComputing (SC), 1996.

Digital Library

[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]

L. Lamport. Time, clocks and ordering of events in distributed systems. Communications of the ACM, 21(7):558--565, July 1978.

Digital Library

[12]

A. L. Lastovetsky, T. Kechadi, and J. Dongarra, editors. Recent Advances in Parallel Virtual Machine and Message Passing Interface, 15th European PVM/MPI Users' Group Meeting, 2008, volume 5205 of Lecture Notes in Computer Science. Springer, 2008.

Digital Library

[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]

M. Musuvathi and S. Qadeer. Fair stateless model checking. In PLDI '08: Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, pages 362--371, New York, NY, USA, 2008. ACM.

Digital Library

[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]

S. Sharma, S. Vakkalanka, G. Gopalakrishnan, R. M. Kirby, R. Thakur, and W. Gropp. A formal approach to detect functionally irrelevant barriers in mpi programs. In Lastovetsky et al. {12}, pages 265--273.

Digital Library

[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]

S. F. Siegel and L. F. Rossi. Analyzing BlobFlow: A case study using model checking to verify parallel scientific software. In Lastovetsky et al. DBLP:conf/pvm/2008, pages 274--282.

Digital Library

[21]

S. F. Siegel and A. R. Siegel. MADRE: The Memory-Aware Data Redistribution Engine. In Lastovetsky et al. {12}, pages 218--226.

Digital Library

[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.

Digital Library

[23]

S. Vakkalanka, M. DeLisi, G. Gopalakrishnan, R. M. Kirby, R. Thakur, and W. Gropp. Implementing efficient dynamic formal verification methods for mpi programs. In Lastovetsky et al. {12}, pages 248--256.

Digital Library

[24]

S. Vakkalanka, G. Gopalakrishnan, and R. M. Kirby.Dynamic verification of MPI programs with reductions in presence of split operations and relaxed orderings. In CAV, volume 5123 of Lecture Notes in Computer Science, pages 66--79. Springer, 2008.

Digital Library

[25]

J. S. Vetter and B. R. de Supinski. Dynamic software testing of MPI applications with Umpire. In Supercomputing, pages 70--79, 2000.

Digital Library

[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.

Digital Library

[27]

Y. Yang, X. Chen, G. Gopalakrishnan, and R. M. Kirby. Efficient stateful dynamic partial order reduction. In SPIN, Lecture Notes in Computer Science, pages 288--305. Springer, 2008.

Digital Library

Cited By

de Oliveira Dantas Ade Carvalho Junior FBarbosa L(2020)A component-based framework for certification of components in a cloud of HPC servicesScience of Computer Programming10.1016/j.scico.2019.102379191:COnline publication date: 1-Jun-2020
https://dl.acm.org/doi/10.1016/j.scico.2019.102379
Lin FLiu YGuo YQian D(2020)ELS: Emulation system for debugging and tuning large-scale parallel programs on small clustersThe Journal of Supercomputing10.1007/s11227-020-03319-677:2(1635-1666)Online publication date: 23-May-2020
https://doi.org/10.1007/s11227-020-03319-6
Ye FZhao JSarkar V(2018)Detecting MPI Usage Anomalies via Partial Program Symbolic ExecutionSC18: International Conference for High Performance Computing, Networking, Storage and Analysis10.1109/SC.2018.00066(794-806)Online publication date: Nov-2018
https://doi.org/10.1109/SC.2018.00066
Show More Cited By

Index Terms

Formal verification of practical MPI programs
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Symbolic verification of message passing interface programs
ICSE '20: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering

Message passing is the standard paradigm of programming in high-performance computing. However, verifying Message Passing Interface (MPI) programs is challenging, due to the complex program features (such as non-determinism and non-blocking operations). ...
Formal verification of practical MPI programs
PPoPP '09: Proceedings of the 14th ACM SIGPLAN symposium on Principles and practice of parallel programming

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 ...
Modeling wildcard-free MPI programs for verification
PPoPP '05: Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming

We give several theorems that can be used to substantially reduce the state space that must be considered in applying finite-state verification techniques, such as model checking, to parallel programs written using a subset of MPI. We illustrate the ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 44, Issue 4

PPoPP '09

April 2009

294 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1594835

Issue’s Table of Contents

PPoPP '09: Proceedings of the 14th ACM SIGPLAN symposium on Principles and practice of parallel programming
February 2009
322 pages
ISBN:9781605583976
DOI:10.1145/1504176
General Chair:
Daniel Reed
Microsoft Research, USA
,
Program Chair:
Vivek Sarkar
Rice University, USA

Copyright © 2009 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 February 2009

Published in SIGPLAN Volume 44, Issue 4

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

70
Total Citations
View Citations
707
Total Downloads

Downloads (Last 12 months)27
Downloads (Last 6 weeks)0

Reflects downloads up to 08 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

de Oliveira Dantas Ade Carvalho Junior FBarbosa L(2020)A component-based framework for certification of components in a cloud of HPC servicesScience of Computer Programming10.1016/j.scico.2019.102379191:COnline publication date: 1-Jun-2020
https://dl.acm.org/doi/10.1016/j.scico.2019.102379
Lin FLiu YGuo YQian D(2020)ELS: Emulation system for debugging and tuning large-scale parallel programs on small clustersThe Journal of Supercomputing10.1007/s11227-020-03319-677:2(1635-1666)Online publication date: 23-May-2020
https://doi.org/10.1007/s11227-020-03319-6
Ye FZhao JSarkar V(2018)Detecting MPI Usage Anomalies via Partial Program Symbolic ExecutionSC18: International Conference for High Performance Computing, Networking, Storage and Analysis10.1109/SC.2018.00066(794-806)Online publication date: Nov-2018
https://doi.org/10.1109/SC.2018.00066
Guthmuller MCorona GQuinson M(2018)System-level state equality detection for the formal dynamic verification of legacy distributed applicationsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2017.12.00496(1-11)Online publication date: Apr-2018
https://doi.org/10.1016/j.jlamp.2017.12.004
Pham AJéron TQuinson M(2017)Verifying MPI Applications with SimGridMCProceedings of the First International Workshop on Software Correctness for HPC Applications10.1145/3145344.3145345(28-33)Online publication date: 12-Nov-2017
https://dl.acm.org/doi/10.1145/3145344.3145345
Suijlen W(2017)Mock BSPlib for Testing and Debugging Bulk Synchronous Parallel SoftwareParallel Processing Letters10.1142/S012962641740001127:01(1740001)Online publication date: Mar-2017
https://doi.org/10.1142/S0129626417400011
Irannejad MTchamgoue GFischmeister S(2017)A Reordering Framework for Testing Message-Passing Systems2017 IEEE 20th International Symposium on Real-Time Distributed Computing (ISORC)10.1109/ISORC.2017.6(109-116)Online publication date: May-2017
https://doi.org/10.1109/ISORC.2017.6
Botbol VChailloux ELe Gall T(2017)Static Analysis of Communicating Processes Using Symbolic TransducersVerification, Model Checking, and Abstract Interpretation10.1007/978-3-319-52234-0_5(73-90)Online publication date: 12-Jan-2017
https://doi.org/10.1007/978-3-319-52234-0_5
Oortwijn WBlom SHuisman M(2016)Future-based Static Analysis of Message Passing ProgramsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.211.7211(65-72)Online publication date: 17-Jun-2016
https://doi.org/10.4204/EPTCS.211.7
Tian TZhang YZhou QZhong P(2016)ModelX: Using Model Checking to Find Design Errors of Cloud Applications2016 IEEE International Conference on Computer and Information Technology (CIT)10.1109/CIT.2016.66(607-610)Online publication date: Dec-2016
https://doi.org/10.1109/CIT.2016.66
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents