Implementation and Optimization of Array Bounds Checking in Accelerate

Abstract

Memory access out of allocated bounds opens the door to many critical exploits and bugs in software. Even though safety is desired in all applications, guarding each interaction with memory introduces significant overhead. Still, some program sequences, thanks to their structure, can never violate allocated memory ranges for any possible input, so their instrumentation is redundant. Array languages, like Accelerate and Futhark, are based on algorithmic blueprints of parallel computation. This thesis lays the ground of bounds checking in Accelerate and shows that its front-end representation carries strong high-level guarantees, enough so that a safe and efficient static analysis can prove that filter, a common parallel pattern that involves data-dependent array restructuring, is safe to execute without any runtime access violation prevention after input is validated. We walk through the design of a method derived from ABCD, an efficient on-demand optimization routine designed for Java JIT compilation that propagates simple difference constraints through an inequality graph. I show how this graph can be populated with information inferred from array combinators and from a simplified SCEV analysis component that models basic recurrences and captures value-ranges for outputs of folds, scans, permute collisions and sequential loops. The generality and effectiveness of the design is showcased on real-world programs, focusing on QuickHull, FlashAttention and Sieve of Eratosthenes with repeated filtering, on all of which it proves that over 85% of dynamically unsafe instructions are statically safe, and removes them to boost performance.