poster

Automatic formal verification of MPI-based parallel programs

Authors:

Stephen F. Siegel,

Timothy K. ZirkelAuthors Info & Claims

PPoPP '11: Proceedings of the 16th ACM symposium on Principles and practice of parallel programming

Pages 309 - 310

https://doi.org/10.1145/1941553.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

Huchant PSaillard EBarthou DBrunie HCarribault P(2018)PARCOACH Extension for a Full-Interprocedural Collectives Verification2018 IEEE/ACM 2nd International Workshop on Software Correctness for HPC Applications (Correctness)10.1109/Correctness.2018.00013(69-76)Online publication date: Nov-2018
https://doi.org/10.1109/Correctness.2018.00013
Hilbrich TWeber MProtze Jde Supinski BNagel WDongarra JHolmes DCollis ALarsson Träff JSmith L(2016)Runtime Correctness Analysis of MPI-3 Nonblocking CollectivesProceedings of the 23rd European MPI Users' Group Meeting10.1145/2966884.2966906(188-197)Online publication date: 25-Sep-2016
https://dl.acm.org/doi/10.1145/2966884.2966906
Bandyopadhyay SBanerjee KKumar ASarkar SGerndt M(2016)Implementing an Efficient Path Based Equivalence Checker for Parallel ProgramsProceedings of the ACM Workshop on Software Engineering Methods for Parallel and High Performance Applications10.1145/2916026.2916027(3-10)Online publication date: 31-May-2016
https://dl.acm.org/doi/10.1145/2916026.2916027
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

Verification of MPI programs using CIVL
EuroMPI '17: Proceedings of the 24th European MPI Users' Group Meeting

CIVL is a framework for verifying concurrent programs. The framework is built around a language, CIVL-C, that extends sequential C with general-purpose primitives that can be used to model a variety of concurrency dialects, including OpenMP, Pthreads, ...
Automatic formal verification of MPI-based parallel programs
PPoPP '11

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

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

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

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 February 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Poster

Conference

PPoPP '11

Sponsor:

SIGPLAN

PPoPP '11: ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming

February 12 - 16, 2011

TX, San Antonio, USA

Acceptance Rates

Overall Acceptance Rate 230 of 1,014 submissions, 23%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

28
Total Citations
View Citations
339
Total Downloads

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

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Huchant PSaillard EBarthou DBrunie HCarribault P(2018)PARCOACH Extension for a Full-Interprocedural Collectives Verification2018 IEEE/ACM 2nd International Workshop on Software Correctness for HPC Applications (Correctness)10.1109/Correctness.2018.00013(69-76)Online publication date: Nov-2018
https://doi.org/10.1109/Correctness.2018.00013
Hilbrich TWeber MProtze Jde Supinski BNagel WDongarra JHolmes DCollis ALarsson Träff JSmith L(2016)Runtime Correctness Analysis of MPI-3 Nonblocking CollectivesProceedings of the 23rd European MPI Users' Group Meeting10.1145/2966884.2966906(188-197)Online publication date: 25-Sep-2016
https://dl.acm.org/doi/10.1145/2966884.2966906
Bandyopadhyay SBanerjee KKumar ASarkar SGerndt M(2016)Implementing an Efficient Path Based Equivalence Checker for Parallel ProgramsProceedings of the ACM Workshop on Software Engineering Methods for Parallel and High Performance Applications10.1145/2916026.2916027(3-10)Online publication date: 31-May-2016
https://dl.acm.org/doi/10.1145/2916026.2916027
Narayanaswamy GYoung MXie T(2015)When truth is efficient: analysing concurrencyProceedings of the 2015 International Symposium on Software Testing and Analysis10.1145/2771783.2771790(141-152)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1145/2771783.2771790
Ng NYoshida N(2015)PabbleService Oriented Computing and Applications10.1007/s11761-014-0172-89:3-4(269-284)Online publication date: 1-Sep-2015
https://dl.acm.org/doi/10.1007/s11761-014-0172-8
Xu ZKamil SSolar-Lezama ADamkroger TDongarra J(2014)MSLProceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis10.1109/SC.2014.31(311-322)Online publication date: 16-Nov-2014
https://dl.acm.org/doi/10.1109/SC.2014.31
Marques EMartins FVasconcelos VNg NMartins N(2013)Towards deductive verification of MPI programs against session typesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.137.9137(103-113)Online publication date: 8-Dec-2013
https://doi.org/10.4204/EPTCS.137.9
Saillard ECarribault PBarthou DDongarra JBlas JCarretero J(2013)Combining static and dynamic validation of MPI collective communicationsProceedings of the 20th European MPI Users' Group Meeting10.1145/2488551.2488555(117-122)Online publication date: 15-Sep-2013
https://dl.acm.org/doi/10.1145/2488551.2488555
Park CSen KIancu CMalony ANemirovsky MMidkiff S(2013)Scaling data race detection for partitioned global address space programsProceedings of the 27th international ACM conference on International conference on supercomputing10.1145/2464996.2465000(47-58)Online publication date: 10-Jun-2013
https://dl.acm.org/doi/10.1145/2464996.2465000
Huang YMercer EMcCarthy JDenney EBultan TZeller A(2013)Proving MCAPI executions are correct using SMTProceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2013.6693063(26-36)Online publication date: 11-Nov-2013
https://dl.acm.org/doi/10.1109/ASE.2013.6693063
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.

Cited By

Index Terms

Recommendations

Verification of MPI programs using CIVL

Automatic formal verification of MPI-based parallel programs

Formal verification of practical MPI programs