Efficient and Correct Stencil Computation via Pattern Matching and Static Typing

TL;DR

This paper presents a new approach for optimizing stencil computations by using pattern matching and static typing in the Ypnos language, enabling safe, efficient, and correct array indexing in Haskell.

Contribution

It introduces a type-safe, declarative language extension that guarantees array boundary safety at compile time, improving optimization and correctness in stencil computations.

Findings

Ypnos enforces boundary safety at compile time

Run-time bounds checking is eliminated

Stencil computations are optimized through pattern matching and static types

Abstract

Stencil computations, involving operations over the elements of an array, are a common programming pattern in scientific computing, games, and image processing. As a programming pattern, stencil computations are highly regular and amenable to optimisation and parallelisation. However, general-purpose languages obscure this regular pattern from the compiler, and even the programmer, preventing optimisation and obfuscating (in)correctness. This paper furthers our work on the Ypnos domain-specific language for stencil computations embedded in Haskell. Ypnos allows declarative, abstract specification of stencil computations, exposing the structure of a problem to the compiler and to the programmer via specialised syntax. In this paper we show the decidable safety guarantee that well-formed, well-typed Ypnos programs cannot index outside of array boundaries. Thus indexing in Ypnos is safe and run-time bounds checking can be eliminated. Program information is encoded as types, using the advanced type-system features of the Glasgow Haskell Compiler, with the safe-indexing invariant enforced at compile time via type checking.