poster

Automatic formal verification of MPI-based parallel programs

Authors:

Stephen F. Siegel,

Timothy K. ZirkelAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 8

Pages 309 - 310

https://doi.org/10.1145/2038037.1941603

Published: 12 February 2011 Publication History

Get Access

Abstract

The Toolkit for Accurate Scientific Software (TASS) is a suite of tools for the formal verification of MPI-based parallel programs used in computational science. TASS can verify various safety properties as well as compare two programs for functional equivalence. The TASS front end takes an integer n ≥ 1 and a C/MPI program, and constructs an abstract model of the program with n processes. Procedures, structs, (multi-dimensional) arrays, heap-allocated data, pointers, and pointer arithmetic are all representable in a TASS model. The model is then explored using symbolic execution and explicit state space enumeration. A number of techniques are used to reduce the time and memory consumed. A variety of realistic MPI programs have been verified with TASS, including Jacobi iteration and manager-worker type programs, and some subtle defects have been discovered. TASS is written in Java and is available from http://vsl.cis.udel.edu/tass under the Gnu Public License.

References

[1]

C. Barrett and C. Tinelli. CVC3. In W. Damm and H. Hermanns, editors, CAV 2007, volume 4590 of LNCS, pages 298--302. Springer.

Digital Library

Google Scholar

[2]

C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. Proc. 8th USENIX Symposium on Operating Systems Design and Implementation, 2008.

Digital Library

Google Scholar

[3]

S. Khurshid, C. S. Pǎsǎreanu, and W. Visser. Generalized symbolic execution for model checking and testing. In H. Garavel and J. Hatcliff, editors, TACAS 2003, volume 2619 of LNCS, pages 553--568.

Digital Library

Google Scholar

[4]

J. C. King. Symbolic execution and program testing. Communications of the ACM, 19 (7): 385--394, 1976.

Digital Library

Google Scholar

[5]

S. F. Siegel. Efficient verification of halting properties for MPI programs with wildcard receives. In R. Cousot, editor, VMCAI 2005, volume 3385 of LNCS, pages 413--429.

Digital Library

Google Scholar

[6]

S. F. Siegel and G. S. Avrunin. Modeling wildcard-free MPI programs for verification. In PPoPP'05, pages 95--106. ACM, 2005.

Digital Library

Google Scholar

[7]

S. F. Siegel and G. S. Avrunin. Verification of halting properties for MPI programs using nonblocking operations. In F. Cappello, T. Hérault, and J. Dongarra, editors, Euro PVM/MPI 2007, volume 4757 of LNCS, pages 326--334. Springer, 2007.

Digital Library

Google Scholar

[8]

S. F. Siegel and T. K. Zirkel. Collective assertions. In R. Jhala and D. Schmidt, editors, VMCAI 2011, volume 6538 of LNCS, pages 387--402.

Digital Library

Google Scholar

[9]

S. F. Siegel, A. Mironova, G. S. Avrunin, and L. A. Clarke. Combining symbolic execution with model checking to verify parallel numerical programs. ACM TOSEM, 17 (2): Article 10, 1--34, 2008.

Digital Library

Google Scholar

[10]

A. Vo, S. Vakkalanka, M. DeLisi, G. Gopalakrishnan, R. M. Kirby, and R. Thakur. Formal verification of practical MPI programs. In PPoPP 2009, pages 261--270. ACM.

Digital Library

Google Scholar

Cited By

View all

Hao JWang MZhang H(2024)Efficient Deadlock Detection in MPI Programs with Path Compression and Focus MatchingProceedings of the 15th Asia-Pacific Symposium on Internetware10.1145/3671016.3674822(467-476)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1145/3671016.3674822
Laurent MSaillard EQuinson M(2021)The MPI Bugs Initiative: a Framework for MPI Verification Tools Evaluation2021 IEEE/ACM 5th International Workshop on Software Correctness for HPC Applications (Correctness)10.1109/Correctness54621.2021.00008(1-9)Online publication date: Nov-2021
https://doi.org/10.1109/Correctness54621.2021.00008
Ivutin AVoloshko A(2020)Method of Formal Verification of Program Code based on Petri Net with Additional Semantic Relations2020 ELEKTRO10.1109/ELEKTRO49696.2020.9130267(1-6)Online publication date: May-2020
https://doi.org/10.1109/ELEKTRO49696.2020.9130267
Show More Cited By

Index Terms

Automatic formal verification of MPI-based parallel programs
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Combining symbolic execution and model checking to verify MPI programs
ICSE '18: Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings

Message Passing Interface (MPI) has become the standard programming paradigm in high performance computing. It is challenging to verify MPI programs because of high parallelism and non-determinism. This paper presents MPI symbolic verifier (MPI-SV), the ...
Formal verification of practical MPI programs
PPoPP '09

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 ...
Automatic formal verification of MPI-based parallel programs
PPoPP '11: Proceedings of the 16th ACM symposium on Principles and practice of parallel programming

The Toolkit for Accurate Scientific Software (TASS) is a suite of tools for the formal verification of MPI-based parallel programs used in computational science. TASS can verify various safety properties as well as compare two programs for functional ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 46, Issue 8

PPoPP '11

August 2011

300 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2038037

Issue’s Table of Contents

PPoPP '11: Proceedings of the 16th ACM symposium on Principles and practice of parallel programming
February 2011
326 pages
ISBN:9781450301190
DOI:10.1145/1941553
General Chair:
Calin Cascaval
Qualcomm Research, USA
,
Program Chair:
Pen-Chung Yew
Academia Sinica, Taiwan and University of Minnesota at Twin Cities, USA

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 February 2011

Published in SIGPLAN Volume 46, Issue 8

Check for updates

Author Tags

Qualifiers

Poster

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
341
Total Downloads

Downloads (Last 12 months)14
Downloads (Last 6 weeks)2

Reflects downloads up to 24 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Hao JWang MZhang H(2024)Efficient Deadlock Detection in MPI Programs with Path Compression and Focus MatchingProceedings of the 15th Asia-Pacific Symposium on Internetware10.1145/3671016.3674822(467-476)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1145/3671016.3674822
Laurent MSaillard EQuinson M(2021)The MPI Bugs Initiative: a Framework for MPI Verification Tools Evaluation2021 IEEE/ACM 5th International Workshop on Software Correctness for HPC Applications (Correctness)10.1109/Correctness54621.2021.00008(1-9)Online publication date: Nov-2021
https://doi.org/10.1109/Correctness54621.2021.00008
Ivutin AVoloshko A(2020)Method of Formal Verification of Program Code based on Petri Net with Additional Semantic Relations2020 ELEKTRO10.1109/ELEKTRO49696.2020.9130267(1-6)Online publication date: May-2020
https://doi.org/10.1109/ELEKTRO49696.2020.9130267
Abadi MKeidar-Barner SPidan DVeksler T(2019)Verifying Parallel Code After Refactoring Using Equivalence CheckingInternational Journal of Parallel Programming10.1007/s10766-017-0548-447:1(59-73)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10766-017-0548-4
Huchant PSaillard EBarthou DCarribault P(2019)Multi-valued Expression Analysis for Collective CheckingEuro-Par 2019: Parallel Processing10.1007/978-3-030-29400-7_3(29-43)Online publication date: 26-Aug-2019
https://dl.acm.org/doi/10.1007/978-3-030-29400-7_3
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
Bakst AGleissenthall KKıcı RJhala R(2017)Verifying distributed programs via canonical sequentializationProceedings of the ACM on Programming Languages10.1145/31339341:OOPSLA(1-27)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3133934
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
Gong DZhang CTian TLi Z(2016)Reducing scheduling sequences of message-passing parallel programsInformation and Software Technology10.1016/j.infsof.2016.09.00380:C(217-230)Online publication date: 1-Dec-2016
https://dl.acm.org/doi/10.1016/j.infsof.2016.09.003
Saillard ECarribault PBarthou D(2015)MPI Thread-Level Checking for MPI+OpenMP ApplicationsEuro-Par 2015: Parallel Processing10.1007/978-3-662-48096-0_3(31-42)Online publication date: 25-Jul-2015
https://doi.org/10.1007/978-3-662-48096-0_3
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.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Index Terms

Recommendations

Combining symbolic execution and model checking to verify MPI programs

Formal verification of practical MPI programs