Efficient Verification Solutions for Message Passing Systems

We examine the problem of automatically and efficiently verifying the absence of communication related bugs in message passing systems, specifically in programs written using Message Passing Interface (MPI) API. A typical debugging or testing tool will fail to achieve this goal because they do not provide any guarantee of coverage of non-deterministic communication matches in a message passing program. While dynamic verification tools do provide such a guarantee, they are quickly rendered useless when an interleaving explosion is witnessed. The general problem is difficult to solve, though we propose that specialized techniques can be developed that can work on top of dynamic verification schedulers thus making them more efficient. In this work, we provide point solutions to deal with the interleaving explosion. Specifically, we present algorithms that accomplish the following tasks: (i) identifying irrelevant message passing operations (Barriers) in MPI programs that add to the verification complexity and degrade application´s performance and (ii) reducing sub-stantially the relevant set of interleavings using symmetry patterns, that needs to be explored for the detection of refusal deadlocks in MPI programs.