Barrier matching for programs with textually unaligned barriers

Barriers, a common synchronization primitive in SPMD-style programs, are used to partition a program into a sequence of parallel phases. Popular parallel programming models, such as MPI and OpenMP, allow barriers to be textually unaligned. Textually unaligned barriers make it difficult for the programmer to understand the synchronization phases in the program, and they can easily lead to synchronization errors. In this paper, we present an interprocedural analysis for matching barriers in a program in order to detect synchronization errors, or, if no such errors exist, to determine the synchronization phases of the program. Our analysis uses a combination of path expressions and interprocedural program slicing to match synchronizing barrier statements. If the barrier matching succeeds, the analysis determines the sets of barrier statements that synchronize together. A matching failure indicates the presence of a synchronization error and the analysis constructs a counter example to illustrate the error. We have implemented the analysis in an MPI checker tool for programs written in C and successfully analyzed the synchronization structure of several MPI benchmarks.