Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, and Lori A. Clarke. Combining symbolic execution with model checking to verify parallel numerical programs. ACM Trans. Softw. Eng. Method., 17(2):1–34, 2008. (This is a revised and expanded version of a paper that appeared in ISSTA '06.). [ DOI | .pdf ]
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.
Stephen F. Siegel and George S. Avrunin. Verification of halting properties for MPI programs using nonblocking operations. In Franck Capello, Thomas Herault, and Jack Dongarra, editors, Recent Advances in Parallel Virtual Machine and Message Passing Interface: 14th European PVM/MPI Users' Group Meeting, volume 4757 of Lecture Notes in Computer Science, pages 326–334, Paris, September 2007. Springer-Verlag. [ DOI | .pdf ]
We show that many important properties of certain MPI programs can be verified by considering only a class of executions in which all communication takes place synchronously. In previous work, we showed that similar results hold for MPI programs that use only blocking communication (and avoid certain other constructs, such as MPI_ANYSOURCE); in this paper we show that the same conclusions hold for programs that also use the nonblocking functions MPI_ISEND, MPI_IRECV, and MPI_WAIT. These facts can be used to dramatically reduce the number of states explored when using model checking techniques to verify properties such as freedom from deadlock in such programs.
Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, and Lori A. Clarke. Using model checking with symbolic execution to verify parallel numerical programs. In Mauro Pezzé, editor, Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 157–168, July 2006. [ DOI | .pdf ]
We present a method to verify the correctness of parallel programs that perform complex numerical computations, including computations involving floating-point arithmetic. The 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 computation, to establish the equivalence of the two programs.
Stephen F. Siegel and George S. Avrunin. Modeling wildcard-free MPI programs for verification. In Symposium on Principles and Practice of Parallel Programming (PPoPP '05), pages 95–106, Chicago, IL, June 2005. [ DOI | .pdf ]
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 utility of these theorems by applying them to a small but realistic example.
George S. Avrunin, Stephen F. Siegel, and Andrew R. Siegel. Finite-state verification for high-performance computing. In Phillip Johnson, editor, Proceedings of the Second International Workshop on Software Engineering for High Performance Computing System Applications, pages 68–73, St. Louis, MO, May 2005. [ DOI | .pdf ]
In this paper, we discuss some preliminary results in applying finite-state verification techniques to high performance parallel codes, with a particular emphasis on scientific programs that employ the widely-used Message Passing Interface (MPI). These results suggest that such techniques may have significant potential for improving both the productivity of developers of parallel scientific programs and the quality of those programs. We also briefly sketch some of the research issues that must be addressed to achieve that potential.
Stephen F. Siegel and George S. Avrunin. Verification of MPI-based software for scientific computation. In Susanne Graf and Laurent Mounier, editors, Model Checking Software: 11th International SPIN Workshop, number 2989 in LNCS, pages 286–303, Barcelona, April 2004. Springer-Verlag. [ DOI | .pdf ]
We explore issues related to the application of finite-state verification techniques to scientific computation software employing the widely-used Message-Passing Interface (MPI). Many of the features of MPI that are important for programmers present significant difficulties for model checking. In this paper, we examine a small parallel program that computes the evolution in time of a discretized function u defined on a 2-dimensional domain and governed by the diffusion equation. Although this example is simple, it makes use of many of the problematic features of MPI. We discuss the modeling of these features and use Spin and INCA to verify several correctness properties for various configurations of this program. Finally, we describe some general theorems that can be used to justify simplifications in finite-state models of MPI programs and that guarantee certain properties must hold for any program using only a particular subset of MPI.
Stephen F. Siegel and George S. Avrunin. Analysis of MPI programs. Technical Report UM-CS-2003-036, Department of Computer Science, University of Massachusetts, 2003. [ .pdf ]
We investigate the application of formal verification techniques to parallel programs that employ the Message Passing Interface (MPI). We develop a formal model of a subset of MPI, and then prove a number of theorems about that model that ameliorate or eliminate altogether the state explosion problem. As an example, we show that if one wishes to verify freedom from deadlock, it suffices to consider only synchronous executions.
This file was generated by bibtex2html 1.99.
![[Back]](/icons/back.gif){kind=icon}
Back to George Avrunin's home page