Speculative improvements to verifiable bounds check elimination

ABSTRACT

As a safety measure, the Java programming language requires bounds checking of array accesses. This usually translates to dynamic checks each time an array element is accessed. Static analysis can help eliminate some of those checks by proving them to be redundant, reducing the runtime overhead. Compilation of Java programs is usually method-based, and dynamic dispatch complicates interprocedural analysis. The result is a severely restricted static analysis. This paper presents a novel combination of two techniques to alleviate this problem. By assuming constraints that cannot safely be inferred from the program, the amount of provable safe bounds can be greatly extended. These constraints, called speculations, can be derived automatically from the program code by an analyzer, which assumes that there will be no violation of the array bounds. To ensure that the speculations hold at runtime, additional checks have to be injected into the code. Finding good speculations that benefit the runtime performance can be expensive. This paper shows that the speculation technique can be combined with a verifiable annotation framework, allowing most of the work to be shifted to compile-time. Experimental results show that this combination of techniques increases the number of eliminated bounds checks and can result in speedups that approach unconditional bounds check removal.

REFERENCES

• 1: Wolfram Amme , Niall Dalton , Jeffery von Ronne , Michael Franz, SafeTSA: a type safe and referentially secure mobile-code representation based on static single assignment form, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.137-147, June 2001, Snowbird, Utah, United States
• 2: 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
• 3: J. M. Bull, L. A. Smith, M. D. Westhead, D. S. Henty, and R. A. Davey. A benchmark suite for high performance Java. Concurrency: Practice and Experience, 12(6):375--388, May 2000.
• 4: Guangyu Chen , Mahmut Kandemir, Verifiable annotations for embedded java environments, Proceedings of the 2005 international conference on Compilers, architectures and synthesis for embedded systems, September 24-27, 2005, San Francisco, California, USA [doi>10.1145/1086297.1086312]
• 5: Christopher Colby , Peter Lee , George C. Necula , Fred Blau , Mark Plesko , Kenneth Cline, A certifying compiler for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.95-107, June 18-21, 2000, Vancouver, British Columbia, Canada
• 6: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java(TM) Language Specification, The (3rd Edition) (Java (Addison-Wesley)), Addison-Wesley Professional, 2005
• 7: Brian Grant , Markus Mock , Matthai Philipose , Craig Chambers , Susan J. Eggers, DyC: an expressive annotation-directed dynamic compiler for C, Theoretical Computer Science, v.248 n.1-2, p.147-199, October 2000 [doi>10.1016/S0304-3975(00)00051-7]
• 8: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 9: Vijay S. Menon , Neal Glew , Brian R. Murphy , Andrew McCreight , Tatiana Shpeisman , Ali-Reza Adl-Tabatabai , Leaf Petersen, A verifiable SSA program representation for aggressive compiler optimization, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.397-408, January 11-13, 2006, Charleston, South Carolina, USA
• 10: Markus Mock , Craig Chambers , Susan J. Eggers, Calpa: a tool for automating selective dynamic compilation, Proceedings of the 33rd annual ACM/IEEE international symposium on Microarchitecture, p.291-302, December 2000, Monterey, California, United States [doi>10.1145/360128.360158]
• 11: José E. Moreira , Samuel P. Midkiff , Manish Gupta, From flop to megaflops: Java for technical computing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.265-295, March 2000 [doi>10.1145/349214.349222]
• 12: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 13: Thi Viet Nga Nguyen , François Irigoin, Efficient and effective array bound checking, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.3, p.527-570, May 2005 [doi>10.1145/1065887.1065893]
• 14: D. Niedzielski, A. Gampe, J. von Ronne, and K. Psarris. A verifiable, control flow aware constraint analyzer for bounds check elimination. Technical Report CS-TR-2008-009, Computer Science, The University of Texas at San Antonio, 2008.
• 15: Feng Qian , Laurie J. Hendren , Clark Verbrugge, A Comprehensive Approach to Array Bounds Check Elimination for Java, Proceedings of the 11th International Conference on Compiler Construction, p.325-342, April 08-12, 2002
• 16: Radu Rugina , Martin C. Rinard, Symbolic bounds analysis of pointers, array indices, and accessed memory regions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.185-235, March 2005 [doi>10.1145/1057387.1057388]
• 17: Ajeet Shankar , S. Subramanya Sastry , Rastislav Bodík , James E. Smith, Runtime specialization with optimistic heap analysis, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 18: Jeffery von Ronne , Andreas Gampe , David Niedzielski , Kleanthis Psarris, Safe bounds check annotations, Concurrency and Computation: Practice & Experience, v.21 n.1, p.41-57, January 2009 [doi>10.1002/cpe.v21:1]
• 19: Thomas Würthinger , Christian Wimmer , Hanspeter Mössenböck, Array bounds check elimination for the Java HotSpot™ client compiler, Proceedings of the 5th international symposium on Principles and practice of programming in Java, September 05-07, 2007, Lisboa, Portugal [doi>10.1145/1294325.1294343]
• 20: Jisheng Zhao , Ian Rogers , Chris Kirkham , Ian Watson, Loop Parallelisation for the Jikes RVM, Proceedings of the Sixth International Conference on Parallel and Distributed Computing Applications and Technologies, p.35-39, December 05-08, 2005 [doi>10.1109/PDCAT.2005.164]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization; Code generation

General Terms:
Algorithms, Languages, Performance

Keywords:
Java, SafeTSA, array bounds check elimination, just-in-time compilation, optimization, verifiable annotations