Arrays computations are at the core of numerical modelling and computational science applications. However, low-level manipulation of array indices is a source of program error. Many practitioners are aware of the need to ensure program correctness, yet very few of the techniques from the programming research community are applied by scientists. We aim to change that by providing targetted lightweight verification techniques for scientific code. We focus on the all too common mistake of array offset errors as a generalisation of off-by-one errors. Firstly, we report on a code analysis study on eleven real-world computational science code base, identifying common idioms of array usage and their spatial properties. This provides much needed data on array programming idioms common in scientific code. From this data, we designed a lightweight declarative specification language capturing the majority of array access patterns via a small set of combinators. We detail a semantic model, and the design and implementation of a verification tool for our specification language, which both checks and infers specifications. We evaluate our tool on our corpus of scientific code. Using the inference mode, we found roughly 93,000 targets for specification across roughly 1.4 million lines of code, showing that the vast majority of array computations read from arrays in a pattern with a simple, regular, static shape. We also studied the commit logs of one of our corpus packages, finding past bug fixes for which our specification system
distinguishes the change and thus could have been applied to detect such bugs.
Thu 26 OctDisplayed time zone: Tijuana, Baja California change
10:30 - 12:00 | Optimizing Compilation and VerificationOOPSLA at Regency C Chair(s): Gregor Richards University of Waterloo | ||
10:30 22mTalk | The Tensor Algebra Compiler OOPSLA Fredrik Kjolstad MIT CSAIL, Shoaib Kamil Adobe, Stephen Chou MIT CSAIL, David Lugato CEA, France, Saman Amarasinghe MIT DOI | ||
10:52 22mTalk | TreeFuser: A Framework for Analyzing and Fusing General Recursive Tree Traversals OOPSLA Laith Sakka Purdue University, Kirshanthan Sundararajah Purdue University, Milind Kulkarni Purdue University DOI | ||
11:15 22mTalk | Verifying Spatial Properties of Array Computations OOPSLA Dominic Orchard University of Kent, UK, Mistral Contrastin , Matthew Danish University of Cambridge, UK, Andrew Rice University of Cambridge, UK DOI | ||
11:37 22mTalk | GLORE: Generalized Loop Redundancy Elimination upon LER-Notation OOPSLA DOI |