Vadim Zaliva and Franz Franchetti (Proc. Workshop on Functional High Performance Computing (FHPC), 2018)
HELIX: A Case Study of a Formal Verification of High Performance Program Generation
Preprint (732 KB)
Published paper (link to publisher)

In this paper, we present HELIX, a formally verified operator language and rewriting engine for generation of high performance implementation for a variety of linear algebra algorithms. Based on the existing SPIRAL system, HELIX adds the rigor of formal verification of its correctness using Coq proof assistant. It formally defines two domain-specific languages: HCOL, which represents a computation data flow and Σ-HCOL, which extends HCOL with iterative computations. A framework for automatically proving semantic preservation of expression rewriting for both languages is presented. The structural properties of the dataflow graph which allow efficient compilation are formalized, and a monadic approach to tracking them and to reasoning about structural correctness of Σ-HCOL expressions is presented.

High performance, Program generation