The message-passing interface (MPI) is a parallel computation standard that is widely used, especially in scientific computing. Parallel computation exhibits specific correctness problems arising from the possibility of several kinds of communication errors, for example, deadlock situations. Especially for complex and costly computations, it can be very important to verify that such situations cannot occur in a given program. There are several approaches available ranging from runtime checking to model checkers that explore and check the communication behavior. This paper adds a further technique, called ParType, based on type checking an MPI program with a protocol specification that is expressed as a type for the program. The problem of verification is then reduced to type checking the program.
The paper starts with an overview section that introduces a finite difference algorithm as a motivating example. The protocol specification language used in verification is then presented with the help of the example. Next, the type theory is formally constructed and some properties of the theory are stated. A message-passing programming language and its reduction semantics are then defined and some important consistency results are stated. The following section explains how the programming language and its protocol type system are encoded within a modified C program with MPI support and how type checking can be performed via the VCC verifier.
The final sections evaluate the performance of this approach in comparison with other verification approaches, compare the approach with other approaches, and look toward future work. The main benefit of this type of verification approach is that the verification time does not depend on the number of processors or iterations; hence, for a large number of iterations, the ParType approach mostly beats the other approaches.
The paper is quite readable and the basic ideas are readily grasped; however, many technical details have been omitted. Furthermore, the sections explaining the verification algorithm are sketchy and assume familiarity with the VCC verifier. Hence, the details may be difficult to comprehend for someone interested in concurrency in general.