Radu Rugina
Skip Abstract Section
Abstract
This article 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.
- Amarasinghe, S., Anderson, J., Lam, M., and Tseng, C. 1995. The SUIF compiler for scalable parallel machines. In Proceedings of the 8th SIAM Conference on Parallel Processing for Scientific Computing (San Francisco, Calif.).]]Google Scholar
- Asuru, J. 1992. Optimization of array subscript range checks. ACM Lett. Prog. Lang. Syst. 1, 2 (June), 109--118.]] Google Scholar
- Austin, T., Breach, S., and Sohi, G. 1994. Efficient detection of all pointer and array access errors. In Proceedings of the SIGPLAN '94 Conference on Program Language Design and Implementation (Orlando, Fla.). ACM, New York.]] Google Scholar
- Balasundaram, V. and Kennedy, K. 1989a. Compile-time detection of race conditions in a parallel program. In Proceedings of the 1989 ACM International Conference on Supercomputing (Crete, Greece). ACM, New York.]] Google Scholar
- Balasundaram, V. and Kennedy, K. 1989b. A technique for summarizing data access and its use in parallelism enhancing transformations. In Proceedings of the SIGPLAN '89 Conference on Program Language Design and Implementation (Portland, Ore.). ACM, New York.]] Google Scholar
- Banerjee, U. 1979. Speedup of ordinary programs. Ph.D. dissertation. Dept. of Computer Science, Univ. of Illinois at Urbana-Champaign, Urbana-Champaign, Ill.]] Google Scholar
- Banerjee, U. 1988. Dependence Analysis for Supercomputing. Kluwer Academic Publishers, Boston, Mass.]] Google Scholar
- Blume, W. and Eigenmann, R. 1995. Symbolic range propagation. In Proceedings of the 9th International Parallel Processing Symposium (Santa Barbara, Calif.).]] Google Scholar
- Blume, W., Eigenmann, R., Faigin, K., Grout, J., Hoeflinger, J., Padua, D., Petersen, P., Pottenger, B., Rauchwerger, L., Tu, P., and Weatherford, S. 1994. Polaris: The next generation in parallelizing compilers. In Proceedings of the 7th Workshop on Languages and Compilers for Parallel Computing (Ithaca, N.Y.).]] Google Scholar
- Blumofe, R., Joerg, C., Kuszmaul, B., Leiserson, C., Randall, K., and Zhou, Y. 1996. Cilk: An efficient multithreaded runtime system. J. Parall. Distrib. Comput. 37, 1 (Aug.), 55--69.]] Google Scholar
- Bodik, R., Gupta, R., and Sarkar, V. 2000. ABCD: Eliminating array bounds checks on demand. In Proceedings of the SIGPLAN '00 Conference on Program Language Design and Implementation (Vancouver, B.C., Canada). ACM, New York.]] Google Scholar
- Bourdoncle, F. 1993. Abstract debugging of higher-order imperative languages. In Proceedings of the SIGPLAN '93 Conference on Program Language Design and Implementation (Albuquerque, N.M.). ACM, New York.]] Google Scholar
- Boyapati, C. and Rinard, M. 2001. A parameterized type system for race-free Java programs. In Proceedings of the 16th Annual Conference on Object-Oriented Programming Systems, Languages and Applications (Tampa Bay, Fla.).]] Google Scholar
- Budiu, M., Goldstein, S., Sakr, M., and Walker, K. 2000. BitValue inference: Detecting and exploiting narrow bitwidth computations. In Proceedings of the EuroPar 2000 European Conference on Parallel Computing (Munich, Germany).]] Google Scholar
- Callahan, D., Kennedy, K., and Subhlok, J. 1990. Analysis of event synchronization in a parallel programming tool. In Proceedings of the 2nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (Seattle, Wash.). ACM, New York.]] Google Scholar
- Chase, D., Wegman, M., and Zadek, F. 1990. Analysis of pointers and structures. In Proceedings of the SIGPLAN '90 Conference on Program Language Design and Implementation (White Plains, N.Y.). ACM, New York.]] Google Scholar
- Chatterjee, S., Lebeck, A., Patnala, P., and Thottethodi, M. 1999. Recursive array layouts and fast matrix multiplication. In Proceedings of the 11th Annual ACM Symposium on Parallel Algorithms and Architectures (Saint Malo, France). ACM, New York.]] Google Scholar
- Cheng, G., Feng, M., Leiserson, C., Randall, K., and Stark, A. 1998. Detecting data races in CILK programs that use locks. In Proceedings of the 10th Annual ACM Symposium on Parallel Algorithms and Architectures (Puerto Vallarta, Mexico). ACM, New York.]] Google Scholar
- Choi, J.-D., Lee, K., Loginov, A., O'Callahan, R., Sarkar, V., and Sridharan, M. 2002. Efficient and precise datarace detection for multithreaded object-oriented programs. In Proceedings of the SIGPLAN '02 Conference on Program Language Design and Implementation (Berlin, Germany).]] Google Scholar
- DeLine, R. and Fahndrich, M. 2001. Enforcing high-level protocols in low-level software. In Proceedings of the SIGPLAN '01 Conference on Program Language Design and Implementation (Snowbird, Ut.).]] Google Scholar
- Detlefs, D., Leino, K. R., Nelson, G., and Saxe, J. 1998. Extended static checking. Tech. Rep. 159, Compaq Systems Research Center.]]Google Scholar
- Dinning, A. and Schonberg, E. 1991. Detecting access anomalies in programs with critical sections. In Proceedings of the ACM/ONR Workshop on Parallel and Distributed Debugging (Santa Cruz, Calif.). ACM, New York.]] Google Scholar
- Duesterwald, E. and Soffa, M. 1991. Concurrency analysis in the presence of procedures using a data-flow framework. In Proceedings of the 1991 International Symposium on Software Testing and Analysis (Victoria, B.C., Canada). ACM, New York.]] Google Scholar
- Emrath, P., Ghosh, S., and Padua, D. 1989. Event synchronization analysis for debugging parallel programs. In Proceedings of Supercomputing '89 (Reno, Nev.).]] Google Scholar
- Emrath, P. and Padua, D. 1988. Automatic detection of nondeterminacy in parallel programs. In Proceedings of the ACM SIGPLAN and SIGOPS Workshop on Parallel and Distributed Debugging (Madison, Wisc.).]] Google Scholar
- Flanagan, C. and Abadi, M. 1999. Types for safe locking. In Proceedings of the 1999 European Symposium on Programming. Amsterdam, The Netherlands.]] Google Scholar
- Flanagan, C. and Freund, S. 2000. Type-based race detection for Java. In Proceedings of the SIGPLAN '00 Conference on Program Language Design and Implementation (Vancouver, B.C., Canada). ACM, New York.]] Google Scholar
- Flanagan, C., Leino, R., Lillibridge, M., Nelson, G., Saxe, J., and Stata, R. 2002. Extended static checking for Java. In Proceedings of the SIGPLAN '02 Conference on Program Language Design and Implementation (Berlin, Germany). ACM, New York.]] Google Scholar
- Flanagan, C. and Qadeer, S. 2003. A type and effect system for atomicity. In Proceedings of the SIGPLAN '03 Conference on Program Language Design and Implementation (San Diego, Calif.). ACM, New York.]] Google Scholar
- Frens, J. and Wise, D. 1997. Auto-blocking matrix-multiplication or tracking BLAS3 performance from source code. In Proceedings of the 6th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (Las Vegas, Nev.). ACM, New York.]] Google Scholar
- Frigo, M., Leiserson, C., and Randall, K. 1998. The implementation of the CILK-5 multithreaded language. In Proceedings of the SIGPLAN '98 Conference on Program Language Design and Implementation (Montreal, Que., Canada). ACM, New York.]] Google Scholar
- Ghiya, R. and Hendren, L. 1996. Is is a tree, a DAG or a cyclic graph? A shape analysis for heap-directed pointers in C. In Proceedings of the 23rd Annual ACM Symposium on the Principles of Programming Languages (St. Petersburg Beach, Fla.). ACM, New York.]] Google Scholar
- Goff, G., Kennedy, K., and Tseng, C. 1991. Practical dependence testing. In Proceedings of the SIGPLAN '91 Conference on Program Language Design and Implementation (Toronto, Ont., Canada). ACM, New York.]] Google Scholar
- Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., and Cheney, J. 2002. Region-based memory management in Cyclone. In Proceedings of the SIGPLAN '02 Conference on Program Language Design and Implementation (Berlin, Germany). ACM, New York.]] Google Scholar
- Gupta, M., Mukhopadhyay, S., and Sinha, N. 1999. Automatic parallelization of recursive procedures. In Proceedings of the International Conference on Parallel Architectures and Compilation Techniques (PACT '99) (Newport Beach, Calif.).]] Google Scholar
- Gupta, R. 1990. A fresh look at optimizing array bound checking. In Proceedings of the SIGPLAN '90 Conference on Program Language Design and Implementation (White Plains, N.Y.). ACM, New York.]] Google Scholar
- Gupta, R. 1993. Optimizing array bound checks using flow analysis. ACM Lett. Prog. Lang. Syst. 2, 1--4 (Mar.-Dec.), 135--150.]] Google Scholar
- Gustavson, F. 1997. Recursion leads to automatic variable blocking for dense linear-algebra algorithms. IBM J. Res. Devel. 41, 6 (Nov.), 737--755.]] Google Scholar
- Hall, M., Amarasinghe, S., Murphy, B., Liao, S., and Lam, M. 1995. Detecting coarse-grain parallelism using an interprocedural parallelizing compiler. In Proceedings of Supercomputing '95 (San Diego, Calif.).]] Google Scholar
- Hall, M. W., Hiranandani, S., Kennedy, K., and Tseng, C. 1992. Interprocedural compilation of Fortran D for MIMD distributed-memory machines. In Proceedings of Supercomputing '92 (Minneapolis, Minn.).]] Google Scholar
- Harrison, W. H. 1977. Compiler analysis of the value ranges for variables. IEEE Trans. Softw. Eng. SE-3, 3 (May), 243--250.]]Google Scholar
- Havlak, P. and Kennedy, K. 1991. An implementation of interprocedural bounded regular section analysis. IEEE Trans. Paral. Distrib. Syst. 2, 3 (July), 350--360.]] Google Scholar
- Kolte, P. and Wolfe, M. 1995. Elimination of redundant array subscript range checks. In Proceedings of the SIGPLAN '95 Conference on Program Language Design and Implementation (San Diego, Calif.). ACM, New York.]] Google Scholar
- Kong, X., Klappholz, D., and Psarris, K. 1990. The I test: A new test for subscript data dependence. In Proceedings of the 1990 International Conference on Parallel Processing (St. Charles, Ill.).]]Google Scholar
- Larochelle, D. and Evans, D. 2001. Statically detecting likely buffer overflow vulnerabilities. In Proceedings of the 10th USENIX Security Symposium (Washington, D.C.).]] Google Scholar
- Markstein, V., Cocke, J., and Markstein, P. 1982. Optimization of range checking. In Proceedings of the SIGPLAN '82 Symposium on Compiler Construction (Boston, Mass.). ACM, New York.]] Google Scholar
- Maydan, D., Hennessy, J., and Lam, M. 1991. Efficient and exact data dependence analysis. In Proceedings of the SIGPLAN '91 Conference on Program Language Design and Implementation (Toronto, Ont., Canada). ACM, New York.]] Google Scholar
- Mellor-Crummey, J. 1991. On-the-fly detection of data races for programs with nested fork-join parallelism. In Proceedings of Supercomputing '91 (Albuquerque, N.M.).]] Google Scholar
- Meyer, B. 1992. Eiffel: The Language. Prentice-Hall, Englewood Cliffs, N.J.]] Google Scholar
- Min, S. and Choi, J. 1991. Race frontier: Reproducing data races in parallel-program debugging. In Proceedings of the 3rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (Williamsburg, Va.). ACM, New York.]] Google Scholar
- Necula, G. and Lee, P. 1998. The design and implementation of a certifying compiler. In Proceedings of the SIGPLAN '98 Conference on Program Language Design and Implementation (Montreal, Que., Canada). ACM, New York.]] Google Scholar
- Netzer, R. and Miller, B. 1991. Improving the accuracy of data race detection. In Proceedings of the 3rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (Williamsburg, Va.). ACM, New York.]] Google Scholar
- Nielson, F., Nielson, H., and Hankin, C. 1999. Principles of Program Analysis. Springer-Verlag, Heidelberg, Germany.]] Google Scholar
- O'Callahan, R. and Choi, J.-D. 2003. Hybrid dynamic data race detection. In Proceedings of the 9th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (San Diego, Calif.). ACM, New York.]] Google Scholar
- Patterson, J. 1995. Accurate static branch prediction by value range propagation. In Proceedings of the SIGPLAN '95 Conference on Program Language Design and Implementation (San Diego, Calif.). ACM, New York.]] Google Scholar
- Pozniansky, E. and Schuster, A. 2003. Efficient on-the-fly data race detection in multihreaded C++ programs. In Proceedings of the 9th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (San Diego, Calif.). ACM, New York.]] Google Scholar
- Praun, C. and Gross, T. 2001. Object race detection. In Proceedings of the 16th Annual Conference on Object-Oriented Programming Systems, Languages and Applications (Tampa Bay, Fla.).]] Google Scholar
- Praun, C. and Gross, T. 2003. Static conflict analysis for multi-threaded object-oriented programs. In Proceedings of the SIGPLAN '03 Conference on Program Language Design and Implementation (San Diego, Calif.). ACM, New York.]] Google Scholar
- Pugh, W. 1991. The Omega test: A fast and practical integer programming algorithm for dependence analysis. In Proceedings of Supercomputing '91 (Albuquerque, N.M.).]] Google Scholar
- Rinard, M. and Diniz, P. 1997. Commutativity analysis: A new analysis technique for parallelizing compilers. ACM Trans. Prog. Lang. Syst. 19, 6 (Nov.), 941--992.]] Google Scholar
- Rugina, R. and Rinard, M. 1999a. Automatic parallelization of divide and conquer algorithms. In Proceedings of the 7th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (Atlanta, Ga.). ACM, New York.]] Google Scholar
- Rugina, R. and Rinard, M. 1999b. Pointer analysis for multithreaded programs. In Proceedings of the SIGPLAN '99 Conference on Program Language Design and Implementation (Atlanta, Ga.). ACM, New York.]] Google Scholar
- Sagiv, M., Reps, T., and Wilhelm, R. 1998. Solving shape-analysis problems in languages with destructive updating. ACM Trans. Prog. Lang. Syst. 20, 1 (Jan.), 1--50.]] Google Scholar
- Sagiv, M., Reps, T., and Wilhelm, R. 2002. Parametric shape analysis via 3-valued logic. ACM Trans. Prog. Lang. Syst. 24, 3 (May).]] Google Scholar
- Savage, S., Burrows, M., Nelson, G., Solbovarro, P., and Anderson, T. 1997. Eraser: A dynamic race detector for multi-threaded programs. ACM Trans. Comput. Syst. 15, 4, 391--411.]] Google Scholar
- Steele, G. 1990. Making asynchronous parallelism safe for the world. In Proceedings of the 17th Annual ACM Symposium on the Principles of Programming Languages (San Francisco, Calif.). ACM, New York.]] Google Scholar
- Steensgaard, B. 1996. Points-to analysis in almost linear time. In Proceedings of the 23rd Annual ACM Symposium on the Principles of Programming Languages (St. Petersburg Beach, Fla.). ACM, New York.]] Google Scholar
- Stephenson, M., Babb, J., and Amarasinghe, S. 2000. Bitwidth analysis with application to silicon compilation. In Proceedings of the SIGPLAN '00 Conference on Program Language Design and Implementation (Vancouver, B.C., Canada). ACM, New York.]] Google Scholar
- Sterling, N. 1994. Warlock: A static data race analysis tool. In Proceedings of the 1993 Winter USENIX Conference (San Diego, Calif.).]]Google Scholar
- Suzuki, N. and Ishihata, K. 1977. Implementation of an array bound checker. In Conference Record of the 4th Annual ACM Symposium on the Principles of Programming Languages (Los Angeles, Calif.). ACM, New York.]] Google Scholar
- Taylor, R. N. 1983. A general purpose algorithm for analyzing concurrent programs. Commun. ACM 26, 5 (May), 362--376.]] Google Scholar
- Triolet, R., Irigoin, F., and Feautrier, P. 1986. Direct parallelization of CALL statements. In Proceedings of the SIGPLAN '86 Symposium on Compiler Construction (Palo Alto, Calif.). ACM, New York.]] Google Scholar
- Verbrugge, C., Co, P., and Hendren, L. 1996. Generalized constant propagation: A study in C. In Proceedings of the 1996 International Conference on Compiler Construction (Linköping, Sweden).]] Google Scholar
- Wagner, D., Foster, J., Brewer, E., and Aiken, A. 2000. A first step towards automated detection of buffer overrun vulnerabilities. In Network and Distributed System Security Symposium (San Diego, Calif.).]]Google Scholar
- Wilson, R. and Lam, M. 1995. Efficient context-sensitive pointer analysis for C programs. In Proceedings of the SIGPLAN '95 Conference on Program Language Design and Implementation (La Jolla, Calif.). ACM, New York.]] Google Scholar
- Wolfe, M. J. 1982. Optimizing supercompilers for supercomputers. Ph.D. dissertation. Dept. of Computer Science, Univ. of Illinois at Urbana-Champaign.]] Google Scholar
- Xi, H. and Pfenning, F. 1998. Eliminating array bound checking through dependent types. In Proceedings of the SIGPLAN '98 Conference on Program Language Design and Implementation (Montreal, Que., Canada). ACM, New York.]] Google Scholar
Index Terms
- Symbolic bounds analysis of pointers, array indices, and accessed memory regions
Recommendations
Symbolic range analysis of pointers
CGO '16: Proceedings of the 2016 International Symposium on Code Generation and OptimizationAlias analysis is one of the most fundamental techniques that compilers use to optimize languages with pointers. However, in spite of all the attention that this topic has received, the current state-of-the-art approaches inside compilers still face ...
Symbolic bounds analysis of pointers, array indices, and accessed memory regions
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 ...
Symbolic bounds analysis of pointers, array indices, and accessed memory regions
PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementationThis 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 ...
Comments