Deriving Correct High-Performance Algorithms

TL;DR

This paper advocates a goal-oriented, formal derivation approach for creating correct high-performance algorithms, demonstrated in dense linear algebra for distributed memory systems, leading to practical software improvements.

Contribution

It introduces a systematic method for deriving correct algorithms in high-performance computing, enabling the discovery of optimal algorithms for specific architectures.

Findings

Algorithms can be systematically derived to be correct.

The approach has been applied to rewrite dense linear algebra software.

Formal methods positively impact high-performance computing software.

Abstract

Dijkstra observed that verifying correctness of a program is difficult and conjectured that derivation of a program hand-in-hand with its proof of correctness was the answer. We illustrate this goal-oriented approach by applying it to the domain of dense linear algebra libraries for distributed memory parallel computers. We show that algorithms that underlie the implementation of most functionality for this domain can be systematically derived to be correct. The benefit is that an entire family of algorithms for an operation is discovered so that the best algorithm for a given architecture can be chosen. This approach is very practical: Ideas inspired by it have been used to rewrite the dense linear algebra software stack starting below the Basic Linear Algebra Subprograms (BLAS) and reaching up through the Elemental distributed memory library, and every level in between. The paper demonstrates how formal methods and rigorous mathematical techniques for correctness impact HPC.