Barrier matching for programs with textually unaligned barriers

ABSTRACT

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.

REFERENCES

• 1: Alexander Aiken , David Gay, Barrier inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.342-354, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268974]
• 2: L. O. Andersen. Program Analysis and Specialization For the C Programming Language. PhD thesis, University of Copenhagen, 1994.
• 3: D. Callahan , K. Kennedy , J. Subhlok, Analysis of event synchronization in a parallel programming tool, Proceedings of the second ACM SIGPLAN symposium on Principles & practice of parallel programming, p.21-30, March 14-16, 1990, Seattle, Washington, United States
• 4: Ron Cytron , Jeanne Ferrante , Barry K. Rosen , Mark N. Wegman , F. Kenneth Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.451-490, Oct. 1991 [doi>10.1145/115372.115320]
• 5: Alain Darte , Robert Schreiber, A linear-time algorithm for optimal barrier placement, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065949]
• 6: Evelyn Duesterwald , Mary Lou Soffa, Concurrency analysis in the presence of procedures using a data-flow framework, Proceedings of the symposium on Testing, analysis, and verification, p.36-48, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120811]
• 7: Ana M. Erosa and Laurie J. Hendren. Taming control flow: A structured approach to eliminating goto statements. In Proceedings of the 1994 International Conference on Computer Languages, pages 229--240, Toulouse, France, May 1994.
• 8: Cormac Flanagan , Stephen N. Freund , Shaz Qadeer , Sanjit A. Seshia, Modular verification of multithreaded programs, Theoretical Computer Science, v.338 n.1-3, p.153-183, 10 June 2005 [doi>10.1016/j.tcs.2004.12.006]
• 9: Susan Horwitz , Thomas Reps , David Binkley, Interprocedural slicing using dependence graphs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.1, p.26-60, Jan. 1990 [doi>10.1145/77606.77608]
• 10: Tor E. Jeremiassen , Susan J. Eggers, Static Analysis of Barrier Synchronization in Explicitly Parallel Programs, Proceedings of the IFIP WG10.3 Working Conference on Parallel Architectures and Compilation Techniques, p.171-180, August 24-26, 1994
• 11: A. Krishnamurthy , D. E. Culler , A. Dusseau , S. C. Goldstein , S. Lumetta , T. von Eicken , K. Yelick, Parallel programming in Split-C, Proceedings of the 1993 ACM/IEEE conference on Supercomputing, p.262-273, December 1993, Portland, Oregon, United States [doi>10.1145/169627.169724]
• 12: Arvind Krishnamurthy , Katherine Yelick, Analyses and optimizations for shared address space programs, Journal of Parallel and Distributed Computing, v.38 n.2, p.130-144, Nov. 1, 1996 [doi>10.1006/jpdc.1996.0136]
• 13: Yuan Lin. Static nonconcurrency analysis of openmp programs. In Fist International Workshop on OpenMP, 2005.
• 14: OpenMP C/C++ Manual. http://www.openmp.org/specs/.
• 15: Stephen P. Masticola , Barbara G. Ryder, Non-concurrency analysis, Proceedings of the fourth ACM SIGPLAN symposium on Principles and practice of parallel programming, p.129-138, May 19-22, 1993, San Diego, California, United States
• 16: Michael O'Boyle , Elena Stöhr, Compile Time Barrier Synchronization Minimization, IEEE Transactions on Parallel and Distributed Systems, v.13 n.6, p.529-543, June 2002 [doi>10.1109/TPDS.2002.1011394]
• 17: Karl J. Ottenstein and Linda M. Ottenstein. The program dependence graph in a software development environment. Software Engineering Notes, 9(3), 1984.
• 18: P. Hulfinger, D. Bonachea, K. Datta, D. Gay, S.Graham, B. Liblit, G. Pike, J. Su, and K. Yelick. Titanium language reference manual. Technical Report UCB/EECS-2005-15, U.C. Berkeley, 2005.
• 19: Shuyi Shao, Alex K. Jones, and Rami Melhem. A compiler-based communication analysis approach for multiprocessor systems, 2006.
• 20: Stephen F. Siegel , George S. Avrunin, Modeling wildcard-free MPI programs for verification, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065957]
• 21: Stephen F. Siegel , Anastasia Mironova , George S. Avrunin , Lori A. Clarke, Using model checking with symbolic execution to verify parallel numerical programs, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146256]
• 22: The Message Passing Interface (MPI) standard. http://www-unix.mcs.anl.gov/mpi/.
• 23: Robert Endre Tarjan, Fast Algorithms for Solving Path Problems, Journal of the ACM (JACM), v.28 n.3, p.594-614, July 1981 [doi>10.1145/322261.322273]
• 24: Robert Endre Tarjan, A Unified Approach to Path Problems, Journal of the ACM (JACM), v.28 n.3, p.577-593, July 1981 [doi>10.1145/322261.322272]
• 25: Steven W. K. Tjiang , John L. Hennessy, Sharlit—a tool for building optimizers, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.82-93, June 15-19, 1992, San Francisco, California, United States
• 26: Chau-Wen Tseng, Compiler optimizations for eliminating barrier synchronization, Proceedings of the fifth ACM SIGPLAN symposium on Principles and practice of parallel programming, p.144-155, July 19-21, 1995, Santa Barbara, California, United States
• 27: Peng Tu , David Padua, Gated SSA-based demand-driven symbolic analysis for parallelizing compilers, Proceedings of the 9th international conference on Supercomputing, p.414-423, July 03-07, 1995, Barcelona, Spain [doi>10.1145/224538.224648]
• 28: G. A. Venkatesh, The semantic approach to program slicing, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.107-119, June 24-28, 1991, Toronto, Ontario, Canada
• 29: Mark Weiser. Program slicing. IEEE Transactions on Software Engineering, 10(4):352--357, July 1984.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
          Subjects: Parallel programming

General Terms:
Verification

Keywords:
MPI, barrier synchronization, path expressions, slicing, static analysis