Write a Blog >>
SPLASH 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Thu 26 Oct 2017 11:15 - 11:37 at Regency C - Optimizing Compilation and Verification Chair(s): Gregor Richards

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 Oct

Displayed 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
22m
Talk
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
22m
Talk
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
22m
Talk
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
22m
Talk
GLORE: Generalized Loop Redundancy Elimination upon LER-Notation
OOPSLA
Yufei Ding North Carolina State University, Xipeng Shen North Carolina State University
DOI