HELIX: a case study of a formal verification of high performance program generation
HELIX: a case study of a formal verification of high performance program generation
复制标题
HELIX：高性能程序生成的形式验证案例研究
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
F. Franchetti
中科院分区：
文献类型：
--
作者：
V. Zaliva;F. Franchetti
在本文中，我们提出了 HELIX，一种经过形式验证的运算符语言和重写引擎，用于生成各种线性代数算法的高性能实现。基于现有的 SPIRAL 系统，HELIX 使用 Coq 证明助手增加了对其正确性的形式验证的严格性。它正式定义了两种特定于领域的语言：HCOL（表示计算数据流）和 Σ-HCOL（通过迭代计算扩展 HCOL）。提出了一种自动证明两种语言的表达式重写的语义保留的框架。允许高效编译的数据流图的结构属性被形式化，并提出了跟踪它们并推理 Σ-HCOL 表达式的结构正确性的一元方法。
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.