Copyrights to these papers may be held by the publishers. The download files are preprints. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

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)
Bibtex

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.

Keywords:
High performance, Program generation