Verifying Properties of Index Arrays in a Purely-Functional Data-Parallel Language

TL;DR

This paper introduces a framework for automatically verifying properties of pure data-parallel programs with non-linear indexing by representing arrays as index functions and using algebraic reasoning, demonstrated in Futhark.

Contribution

It presents a novel approach to verify properties of data-parallel programs with non-linear indexing through index functions and algebraic reasoning, enabling practical and automatic verification.

Findings

Average verification time of 1 second on seven applications

Eliminating dynamic verification leads to significant GPU speedups

Framework extends beyond correctness to enable compiler optimizations

Abstract

This paper presents a novel approach to automatically verify properties of pure data-parallel programs with non-linear indexing -- expressed as pre- and post-conditions on functions. Programs consist of nests of second-order array combinators (e.g., map, scan, and scatter) and loops. The key idea is to represent arrays as index functions: programs are index function transformations over which properties are propagated and inferred. Our framework proves properties on index functions by distilling them into algebraic (in)equalities and discharging them to a Fourier-Motzkin-based solver. The framework is practical and accessible: properties are not restricted to a decidable logic, but instead are carefully selected to express practically useful guarantees that can be automatically reasoned about and inferred. These guarantees extend beyond program correctness and can be exploited by the entire compiler pipeline for optimization. We implement our system in the pure data-parallel language Futhark and demonstrate its practicality on seven applications, reporting an average verification time of 1 second. Two case studies show how eliminating dynamic verification in GPU programs results in significant speedups.