| Abstract |
Writing correct parallel programs is notoriously difficult. For
example, programs may deadlock, or behave non deterministically, or
fail in many ways that prove difficult or impossible to reproduce.
In theory, Finite State Verification (FSV) techniques, such as model
checking, can deal with precisely these issues. But while FSV techniques
have been applied successfully in other contexts, parallel scientific
software poses new and special challenges. In this talk, we will summarize
recent progress in confronting these challenges, including (1) theoretical
results that make it much easier to prove properties of programs that are
restricted to a subset of MPI, (2) MPI-specific optimizations to the
standard model-checking algorithms that can dramatically reduce the number
of states explored, and (3) techniques that combine FSV and symbolic
computation methods in order to prove that the actual calculations
performed by an MPI program are correct.
|
