skip to main content
research-article

Combining symbolic execution with model checking to verify parallel numerical programs

Published: 05 May 2008 Publication History

Abstract

We present a method to verify the correctness of parallel programs that perform complex numerical computations, including computations involving floating-point arithmetic. This method requires that a sequential version of the program be provided, to serve as the specification for the parallel one. The key idea is to use model checking, together with symbolic execution, to establish the equivalence of the two programs. In this approach the path condition from symbolic execution of the sequential program is used to constrain the search through the parallel program. To handle floating-point operations, three different types of equivalence are supported. Several examples are presented, demonstrating the approach and actual errors that were found. Limitations and directions for future research are also described.

References

[1]
Ball, T. and Rajamani, S. K. 2001. Automatically validating temporal safety properties of interfaces. In Proceedings of the 8th International SPIN Workshop. Toronto, Canada, M. B. Dwyer, Ed. Lecture Notes in Computer Science, vol. 2057. Springer-Verlag, 103--122.
[2]
Barner, S., Eisner, C., Glazberg, Z., Kroening, K., and Rabinovitz, I. 2006. ExpliSat: Guiding SAT-based software verification with explicit states. In Proceedings of the 2nd International Haifa Verification Conference. Lecture Notes in Computer Science, vol. 4383. Springer-Verlag, 138--154.
[3]
Boyer, R. S., Elspas, B., and Levitt, K. N. 1975. SELECT---a formal system for testing and debugging programs by symbolic execution. In Proceedings of the International Conference on Reliable Software. ACM Press, 234--245.
[4]
Brand, D. and W. H. Joyner, J. 1978. Verification of protocols using symbolic execution. Comput. Netw. 2, 351--360.
[5]
Clarke, L. A. 1976. A system to generate test data and symbolically execute programs. IEEE Trans. Soft. Engin. 2, 3, 215--222.
[6]
Dillon, L. K. 1990. Using symbolic execution for verification of ada tasking programs. ACM Trans. Program. Lang. Syst. 12, 4, 643--669.
[7]
Elmas, T., Tasiran, S., and Qadeer, S. 2005. VYRD: Verifying concurrent programs by runtime refinement-violation detection. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '05). ACM Press, New York, NY, 27--37.
[8]
Goldberg, D. 1991. What every computer scientist should know about floating-point arithmetic. ACM Comput. Surv. 23, 1, 5--48.
[9]
Gropp, W., Lusk, E., and Skjellum, A. 1999. Using MPI: Portable Parallel Programming with the Message-Passing Interface. MIT Press.
[10]
Hantler, S. L. and King, J. C. 1976. An introduction to proving the correctness of programs. ACM Comput. Surv. 8, 3, 331--353.
[11]
Holzmann, G. J. 2004. The Spin Model Checker. Addison-Wesley.
[12]
IEEE. 1985. 754-1985 IEEE standard for binary floating-point arithmetic.
[13]
IEEE. 1987. 854-1987 IEEE standard for radix-independent floating-point arithmetic.
[14]
Karniadakis, G. E. and Kirby II, R. M. 2003. Parallel Scientific Computing in C++ and MPI. Cambridge University Press.
[15]
Khurshid, S., Păsăreanu, C. S., and Visser, W. 2003. Generalized symbolic execution for model checking and testing. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference (TACAS2003). Warsaw, Poland. H. Garavel and J. Hatcliff, Eds. Lecture Notes in Computer Science, vol. 2619. Springer-Verlag, 553--568.
[16]
Lim, A. W., Cheong, G. I., and Lam, M. S. 1999. An affine partitioning algorithm to maximize parallelism and minimize communication. In Proceedings of the 13th International Conference on Supercomputing (ICC'99). ACM Press, New York, NY, 228--237.
[17]
Martel, M. 2005. An overview of semantics for the validation of numerical programs. In Proceedings of the 6th International Conference on Verification, Model Cheking, and Abstract Interpretation (VMCAI'05). R. Cousot, Ed. Lecture Notes in Computer Science, vol. 3385. 59--77.
[18]
Matlin, O. S., Lusk, E., and McCune, W. 2002. SPINning parallel systems software. In Proceedings of the 9th International SPIN Workshop, D. Bosnacki and S. Leue, Eds. Lecture Notes in Computer Science, vol. 2318. Springer-Verlag, 213--220.
[19]
Message Passing Interface Forum. 1995. MPI: A Message-Passing Interface standard, version 1.1. http://www.mpi-forum.org/docs/.
[20]
Message Passing Interface Forum. 1997. MPI-2: Extensions to the Message-Passing Interface. http://www.mpi-forum.org/docs/.
[21]
Palmer, R., Delisi, M., Gopalakrishnan, G., and Kirby, R. M. 2007. An approach to formalization and analysis of message passing libraries. In Proceedings of the 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS). Springer.
[22]
Palmer, R., Gopalakrishnan, G., and Kirby, R. M. 2007. Semantics driven partial-order reduction of MPI-based parallel programs. In Proceedings of the ACM Workshop on Parallel and Distributed Systems Testing and Debugging (PADTAD). ACM Press, New York, NY, 43--53.
[23]
Păsăreanu, C. S. and Visser, W. 2004. Verification of Java programs using symbolic execution and invariant generation. In Proceedings of the 11th International Spin Workshop. S. Graf and L. Mounier, Eds. Lecture Notes in Computer Science, vol. 2989. Springer-Verlag, 164--181.
[24]
Pervez, S., Gopalakrishnan, G., Kirby, R. M., Palmer, R., Thakur, R., and Gropp, W. 2007. Practical model checking method for verifying correctness of MPI programs. In Proceedings of the 14th European PVM/MPI User's Group Meeting. F. Cappello, T. Herault, and J. Dongarra, Eds. Lecture Notes in Computer Science, vol. 4757. Springer-Verlag.
[25]
Pervez, S., Gopalakrishnan, G., Kirby, R. M., Thakur, R., and Gropp, W. 2006. Formal verification of programs that use MPI one-sided communication. In Recent Advances in Parallel Virtual Machine and Message Passing Interface, B. Mohr, J. L. Träff, J. Worrington, and J. Dongarra, Eds. Lecture Notes in Computer Science, vol. 4192. 30--39.
[26]
Robby, Dwyer, M. B., and Hatcliff, J. 2003. Bogor: an extensible and highly-modular software model checking framework. In Proceedings of the 9th European Software Engineering Conference and the ACM Symposium on the Foundations of Software Engineering. ACM Press, 267--276.
[27]
Rotman, J. J. 1995. An Introduction to the Theory of Groups, 4th Ed. Springer. Berlin, Germany.
[28]
Siegel, S. F. 2004. Efficient verification of halting properties for MPI programs with wildcard receives. Tech. rep. UM-CS-2004-77, Department of Computer Science, University of Massachusetts.
[29]
Siegel, S. F. 2005. Efficient verification of halting properties for MPI programs with wildcard receives. In Proceedings of the 6th International Conference on Verification Model Checking and Abstract Interpretation (VMCAI'05). R. Cousot, Ed. Lecture Notes in Computer Science, vol. 3385. Springer-Verlag. 413--429.
[30]
Siegel, S. F. 2007a. The Mpi-Spin web page. http://vsl.cis.udel.edu/mpi-spin.
[31]
Siegel, S. F. 2007b. Model checking nonblocking MPI programs. In Proceedings of the 8th International Conference Verification, Model Checking, and Abstract Interpretation: (VMCAI2007), Nice, France, B. Cook and A. Podelski, Eds. Lecture Notes in Computer Science, vol. 4349. 44--58.
[32]
Siegel, S. F. and Avrunin, G. S. 2004. Verification of MPI-based software for scientific computation. In Proceedings of the 11th International Spin Workshop. S. Graf and L. Mounier, Eds. Lecture Notes in Computer Science, vol. 2989, Springer-Verlag. 286--303.
[33]
Siegel, S. F. and Avrunin, G. S. 2005. Modeling wildcard-free MPI programs for verification. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. (PPoPP'05), Chicago. ACM Press, 95--106.
[34]
Siegel, S. F. and Avrunin, G. S. 2007. Verification of halting properties for MPI programs using nonblocking operations. In Proceedings of the 14th European PVM/MPI Users's Group Meeting. F. Cappello, T. Herault, and J. Dongarra, Eds. Lecture Notes in Computer Science, vol. 4757. Springer-Verlag, 326--334.
[35]
Snir, M., Otto, S., Huss-Lederman, S., Walker, D., and Dongarra, J. 1998. MPI---The Complete Reference, Volume 1: The MPI Core, 2nd Ed. MIT Press.
[36]
Tomb, A., Brat, G., and Visser, W. 2007. Variably interprocedural program analysis for runtime error detection. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA2007). ACM, 97--107.

Cited By

View all
  • (2024)Symbolic Execution for Quantum Error Correction ProgramsProceedings of the ACM on Programming Languages10.1145/36564198:PLDI(1040-1065)Online publication date: 20-Jun-2024
  • (2024)Collective Contracts for Message-Passing Parallel ProgramsComputer Aided Verification10.1007/978-3-031-65630-9_3(44-68)Online publication date: 24-Jul-2024
  • (2023)Intelligent Constraint Classification for Symbolic Execution2023 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER56733.2023.00023(144-154)Online publication date: Mar-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Software Engineering and Methodology
ACM Transactions on Software Engineering and Methodology  Volume 17, Issue 2
April 2008
207 pages
ISSN:1049-331X
EISSN:1557-7392
DOI:10.1145/1348250
Issue’s Table of Contents
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: 05 May 2008
Accepted: 01 June 2007
Received: 01 April 2007
Published in TOSEM Volume 17, Issue 2

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Finite-state verification
  2. MPI
  3. Message Passing Interface
  4. Spin
  5. concurrency
  6. floating-point
  7. high performance computing
  8. model checking
  9. numerical program
  10. parallel programming
  11. symbolic execution

Qualifiers

  • Research-article
  • Research
  • Refereed

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)18
  • Downloads (Last 6 weeks)1
Reflects downloads up to 22 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Symbolic Execution for Quantum Error Correction ProgramsProceedings of the ACM on Programming Languages10.1145/36564198:PLDI(1040-1065)Online publication date: 20-Jun-2024
  • (2024)Collective Contracts for Message-Passing Parallel ProgramsComputer Aided Verification10.1007/978-3-031-65630-9_3(44-68)Online publication date: 24-Jul-2024
  • (2023)Intelligent Constraint Classification for Symbolic Execution2023 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER56733.2023.00023(144-154)Online publication date: Mar-2023
  • (2022)A Mathematical Model of Parallel Programs and an Approach to Verification of MPI Programs Based on the Proposed ModelAutomatic Control and Computer Sciences10.3103/S014641162207015X56:7(762-777)Online publication date: 1-Dec-2022
  • (2021)A Mathematical Model of Parallel Programs and an Approach Based on it to Verification of MPI ProgramsModeling and Analysis of Information Systems10.18255/1818-1015-2021-4-394-41228:4(394-412)Online publication date: 18-Dec-2021
  • (2021)Predoo: precision testing of deep learning operatorsProceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3460319.3464843(400-412)Online publication date: 11-Jul-2021
  • (2019)Symbolic execution-driven extraction of the parallel execution plans of Spark applicationsProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3338973(246-256)Online publication date: 12-Aug-2019
  • (2019)Big-Data Applications as Self-Adaptive Systems of Systems2019 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)10.1109/ISSREW.2019.00066(155-162)Online publication date: Oct-2019
  • (2019)Bounded Verification of Sparse Matrix Computations2019 IEEE/ACM 3rd International Workshop on Software Correctness for HPC Applications (Correctness)10.1109/Correctness49594.2019.00010(36-43)Online publication date: Nov-2019
  • (2019)Smart Contract Defect Detection Based on Parallel Symbolic Execution2019 3rd International Conference on Circuits, System and Simulation (ICCSS)10.1109/CIRSYSSIM.2019.8935603(127-132)Online publication date: Jun-2019
  • Show More Cited By

View Options

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media