Symbolic bounds analysis of pointers, array indices, and accessed memory regions

ABSTRACT

This paper presents a novel framework for the symbolic bounds analysis of pointers, array indices, and accessed memory regions. Our framework formulates each analysis problem as a system of inequality constraints between symbolic bound polynomials. It then reduces the constraint system to a linear program. The solution to the linear program provides symbolic lower and upper bounds for the values of pointer and array index variables and for the regions of memory that each statement and procedure accesses. This approach eliminates fundamental problems associated with applying standard fixed-point approaches to symbolic analysis problems. Experimental results from our implemented compiler show that the analysis can solve several important problems, including static race detection, automatic parallelization, static detection of array bounds violations, elimination of array bounds checks, and reduction of the number of bits used to store computed values.

REFERENCES

• 1: Saman P. Amarasinghe , Jennifer-Ann M. Anderson , Monica S. Lam , Amy W. Lim, An Overview of a Compiler for Scalable Parallel Machines, Proceedings of the 6th International Workshop on Languages and Compilers for Parallel Computing, p.253-272, August 12-14, 1993
• 2: C. Scott Ananian. Silicon C: A hardware backend for SUIF. Available from http://flex-compiler.lcs.mit.edu/SiliconC/ paper.pdf, May 1998.
• 3: W. Blume, R. Eigenmann, K. Faigin, J. Grout, J. Hoeflinger, D. Padua, P. Petersen, W. Pottenger, L. Raughwerger, P. Tu, and S. Weatherford. Effective automatic parallelization with Polaris. In International Journal of Parallel Programming, May 1995.
• 4: Robert D. Blumofe , Christopher F. Joerg , Bradley C. Kuszmaul , Charles E. Leiserson , Keith H. Randall , Yuli Zhou, Cilk: an efficient multithreaded runtime system, Journal of Parallel and Distributed Computing, v.37 n.1, p.55-69, Aug. 25, 1996 [doi>10.1006/jpdc.1996.0107]
• 5: Rastislav Bodík , Rajiv Gupta , Vivek Sarkar, ABCD: eliminating array bounds checks on demand, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.321-333, June 18-21, 2000, Vancouver, British Columbia, Canada
• 6: Mihai Budiu , Majd Sakr , Kip Walker , Seth Copen Goldstein, BitValue Inference: Detecting and Exploiting Narrow Bitwidth Computations, Proceedings from the 6th International Euro-Par Conference on Parallel Processing, p.969-979, August 29-September 01, 2000
• 7: David R. Chase , Mark Wegman , F. Kenneth Zadeck, Analysis of pointers and structures, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.296-310, June 1990, White Plains, New York, United States
• 8: Siddhartha Chatterjee , Alvin R. Lebeck , Praveen K. Patnala , Mithuna Thottethodi, Recursive array layouts and fast parallel matrix multiplication, Proceedings of the eleventh annual ACM symposium on Parallel algorithms and architectures, p.222-231, June 27-30, 1999, Saint Malo, France [doi>10.1145/305619.305645]
• 9: Guang-Ien Cheng , Mingdong Feng , Charles E. Leiserson , Keith H. Randall , Andrew F. Stark, Detecting data races in Cilk programs that use locks, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.298-309, June 28-July 02, 1998, Puerto Vallarta, Mexico [doi>10.1145/277651.277696]
• 10: D. Detlefs, K. R. Leino, G. Nelson, and J. Saxe. Extended static checking. Technical Report 159, Compaq Systems Research Center, 1998.
• 11: Anne Dinning , Edith Schonberg, Detecting access anomalies in programs with critical sections, Proceedings of the 1991 ACM/ONR workshop on Parallel and distributed debugging, p.85-96, May 20-21, 1991, Santa Cruz, California, United States
• 12: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 13: Jeremy D. Frens , David S. Wise, Auto-blocking matrix-multiplication or tracking BLAS3 performance from source code, Proceedings of the sixth ACM SIGPLAN symposium on Principles and practice of parallel programming, p.206-216, June 18-21, 1997, Las Vegas, Nevada, United States
• 14: Matteo Frigo , Charles E. Leiserson , Keith H. Randall, The implementation of the Cilk-5 multithreaded language, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.212-223, June 17-19, 1998, Montreal, Quebec, Canada
• 15: Manish Gupta , Sayak Mukhopadhyay , Navin Sinha, Automatic Parallelization of Recursive Procedures, Proceedings of the 1999 International Conference on Parallel Architectures and Compilation Techniques, p.139, October 12-16, 1999
• 16: F. G. Gustavson, Recursion leads to automatic variable blocking for dense linear-algebra algorithms, IBM Journal of Research and Development, v.41 n.6, p.737-756, Nov. 1997
• 17: M. W. Hall , S. Hiranandani , K. Kennedy , C.-W. Tseng, Interprocedural compilation of Fortran D for MIMD distributed-memory machines, Proceedings of the 1992 ACM/IEEE conference on Supercomputing, p.522-534, November 16-20, 1992, Minneapolis, Minnesota, United States
• 18: P. Havlak , K. Kennedy, An Implementation of Interprocedural Bounded Regular Section Analysis, IEEE Transactions on Parallel and Distributed Systems, v.2 n.3, p.350-360, July 1991 [doi>10.1109/71.86110]
• 19: Priyadarshan Kolte , Michael Wolfe, Elimination of redundant array subscript range checks, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.270-278, June 18-21, 1995, La Jolla, California, United States
• 20: Victoria Markstein , John Cocke , Peter Markstein, Optimization of range checking, Proceedings of the 1982 SIGPLAN symposium on Compiler construction, p.114-119, June 23-25, 1982, Boston, Massachusetts, United States
• 21: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 22: Jason R. C. Patterson, Accurate static branch prediction by value range propagation, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.67-78, June 18-21, 1995, La Jolla, California, United States
• 23: Martin C. Rinard , Pedro C. Diniz, Commutativity analysis: a new analysis technique for parallelizing compilers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.6, p.942-991, Nov. 1997 [doi>10.1145/267959.269969]
• 24: Radu Rugina , Martin Rinard, Automatic parallelization of divide and conquer algorithms, Proceedings of the seventh ACM SIGPLAN symposium on Principles and practice of parallel programming, p.72-83, May 04-06, 1999, Atlanta, Georgia, United States
• 25: Radu Rugina , Martin Rinard, Pointer analysis for multithreaded programs, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.77-90, May 01-04, 1999, Atlanta, Georgia, United States
• 26: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.1-50, Jan. 1998 [doi>10.1145/271510.271517]
• 27: Mark Stephenson , Jonathan Babb , Saman Amarasinghe, Bidwidth analysis with application to silicon compilation, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.108-120, June 18-21, 2000, Vancouver, British Columbia, Canada
• 28: N. Sterling. Warlock: A static data race analysis tool. In Proceedings of the 1993 Winter Usenix Conference, January 1994.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.3 MEMORY STRUCTURES

Additional Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION

General Terms:
Algorithms, Design, Experimentation, Theory