Repository logo
 

Verifying Spatial Properties of Array Computations

Published version
Peer-reviewed

Type

Article

Change log

Authors

Orchard, D 
Contrastin, M 
Rice, AC 

Abstract

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 veriication techniques for scientiic code. We focus on the all too common mistake of array ofset errors as a generalisation of of-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 scientiic code. From this data, we designed a lightweight declarative speciication 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 veriication tool for our speciication language, which both checks and infers speciications. We evaluate our tool on our corpus of scientiic code. Using the inference mode, we found roughly 87,000 targets for speciication across roughly 1.1 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, inding past bug ixes for which our speciication system distinguishes the change and thus could have been applied to detect such bugs.

Description

Keywords

verification, static-analysis, scientific computing, arrays, stencils

Journal Title

Proceedings of the ACM on Programming Languages

Conference Name

Journal ISSN

2475-1421
2475-1421

Volume Title

1

Publisher

ACM
Sponsorship
Engineering and Physical Sciences Research Council (EP/M026124/1)
This work was supported by the EPSRC [grant number EP/M026124/1].
Relationships
Is supplemented by:
Is source of: