Bounds checking: an instance of hybrid analysis

TY - GEN

T1 - Bounds checking

T2 - ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming 2014

AU - Henriksen, Troels

AU - Oancea, Cosmin Eugen

PY - 2014/6/9

Y1 - 2014/6/9

N2 - This paper presents an analysis for bounds checking of array subscripts that lifts checking assertions to program level under the form of an arbitrarily-complex predicate (inspector), whose runtime evaluation guards the execution of the code of interest. Separating the predicate from the computation makes it more amenable to optimization, and allows it to be split into a cascade of sufficient conditions of increasing complexity that optimizes the commoninspection path. While synthesizing the bounds checking invariant resembles type checking techniques, we rely on compiler simplification and runtime evaluation rather than employing complex inference and annotation systems that might discourage the nonspecialist user. We integrate the analysis in the compiler's repertoire of Futhark: a purely-functional core language supporting mapreduce nested parallelism on regular arrays, and show how the highlevel language invariants enable a relatively straightforward analysis. Finally, we report a qualitative evaluation of our technique on three real-world applications from the financial domain that indicates that the runtime overhead of predicates is negligible..

AB - This paper presents an analysis for bounds checking of array subscripts that lifts checking assertions to program level under the form of an arbitrarily-complex predicate (inspector), whose runtime evaluation guards the execution of the code of interest. Separating the predicate from the computation makes it more amenable to optimization, and allows it to be split into a cascade of sufficient conditions of increasing complexity that optimizes the commoninspection path. While synthesizing the bounds checking invariant resembles type checking techniques, we rely on compiler simplification and runtime evaluation rather than employing complex inference and annotation systems that might discourage the nonspecialist user. We integrate the analysis in the compiler's repertoire of Futhark: a purely-functional core language supporting mapreduce nested parallelism on regular arrays, and show how the highlevel language invariants enable a relatively straightforward analysis. Finally, we report a qualitative evaluation of our technique on three real-world applications from the financial domain that indicates that the runtime overhead of predicates is negligible..

U2 - 10.1145/2627373.2627388

DO - 10.1145/2627373.2627388

M3 - Article in proceedings

SN - 978-1-4503-2937-8

SP - 88

EP - 94

BT - Proceedings of ACM SIGPLAN International Workshop on Libraries, Languages, and Compilers for Array Programming

PB - Association for Computing Machinery

Y2 - 12 June 2014 through 13 June 2014

ER -