MPISE: Symbolic Execution of MPI Programs

TL;DR

MPISE is a symbolic execution tool designed for MPI programs that improves bug detection by covering input and non-determinism, effectively identifying deadlocks and runtime bugs in parallel applications.

Contribution

The paper introduces MPISE, a novel symbolic execution approach with an on-the-fly scheduling algorithm for MPI programs, enhancing bug detection coverage and efficiency.

Findings

MPISE effectively detects deadlocks and runtime bugs.

The tool provides diagnostic information and replay capabilities.

Experimental results show high bug detection efficiency.

Abstract

Message Passing Interfaces (MPI) plays an important role in parallel computing. Many parallel applications are implemented as MPI programs. The existing methods of bug detection for MPI programs have the shortage of providing both input and non-determinism coverage, leading to missed bugs. In this paper, we employ symbolic execution to ensure the input coverage, and propose an on-the-fly schedule algorithm to reduce the interleaving explorations for non-determinism coverage, while ensuring the soundness and completeness. We have implemented our approach as a tool, called MPISE, which can automatically detect the deadlock and runtime bugs in MPI programs. The results of the experiments on benchmark programs and real world MPI programs indicate that MPISE finds bugs effectively and efficiently. In addition, our tool also provides diagnostic information and replay mechanism to help understanding bugs.