Verification of Message Passing Programs

by
Robert Palmer

Advised by
Ganesh Gopalakrishnan

The primary optimization that makes computation fast is parallelism. Many seek to explicitly leverage this parallelism using clusters or shared memory super computers. It is difficult to write a correct and fast distributed computation.

One problem that makes distributed computation difficult is nondeterminism resulting from the concurrency users seek to exploit. Such nondeterminism may cause a range of problems from incorrect results to unpredictable and difficult to trace deadlocks.

Formal Methods have been applied to find difficult to detect errors in both hardware and software systems with dramatic results. We seek to apply such methods as Model Checking, Abstraction Refinement, Satisfiability checking and other techniques to guarantee the absence of such errors in message passing programs.

Present research includes (1) extracting models from C program source using MPI to communicate. (2) Building abstraction refinement and analysis tools to manipulate and simplify the model to be verified. (3) Creation of an environment model in which a C model may maintain data structures, pointers, heap, and other important language features.

In the future we will be applying our verification techniques to MPI based programs from the scientific domain. We plan to use optimizations such as partial order reduction, symmetry reduction, and abstraction refinement to increase the efficiency of the model checking task. In addition we will seek to use brute force via parallel model checking and probabilistic representations to further enhance our effectiveness.