Array bound checking is an important step in software verification, and omitting this step often has consequences ranging from meaningless data to potential security violations. However, such checking is resource-intensive, and, according to the authors, commercial compilers available today are inefficient in implementing these checks. Specifically, these compilers slow down significantly during both compilation and execution, fail to provide sufficient debugging information, and do not check consistency between the sizes of actual and formal array parameters in subroutine calls.

The authors present two optimization techniques for bound checking that improve both the speed and the debugging capability. Broadly speaking, these are the elimination approach, which adds checks at all array references and then removes redundant checks; and the insertion approach, which adds checks only when one cannot prove the references as illegal otherwise. A new algorithm for checking the consistency between the formal and actual parameters is also presented.

The paper contains a comprehensive survey of related work, and highlights the salient features of each approach. Next, it presents a detailed description of PIPS, a source-to-source FORTRAN compiler, used by the authors. Detailed algorithms, examples, and relevant proofs are included.

I believe that the most interesting part of this paper is the experimental results section, where the authors compare the efficiency of their approach for various metrics: removed checks, debugging information, compilation times, execution times, and actual/formal array bounds checking. Using industry-standard benchmarks, they compare their approach with three commercial compilers, and find the results quite promising. In each case, their approach works much better, and they draw several useful conclusions. For instance, the percentage of removed checks may not be a good indicator of the efficiency of an approach. For example, removing a single check in an inner loop may be more effective than removing several checks elsewhere. In addition, the insertion approach generally works better than the elimination approach.

However, by the authors’ own admission, substantial work still needs to be done to apply their approach to languages such as C and Java. These involve handling recursive calls, data structures, pointer arithmetic, and so on, so the effect of their approach may be limited in these languages.

Overall, this paper offers a comprehensive overview of the state of the art in array bounds checking for FORTRAN, and offers promising approaches for improving the efficiency of these checks. Commercial FORTRAN compilers should benefit by adopting this approach.