HELIX

The HELIX project enables the synthesis of high-performance implementations of numerical algorithms by providing a certified compiler for formally specified domain-specific languages (DSLs). Building on the existing SPIRAL system, HELIX enhances the rigour of formal verification using the Coq proof assistant to ensure correctness. It formally defines a series of domain-specific languages, starting with HCOL, which represents computational data flow. HELIX then transforms the original program through a series of intermediate languages, culminating in LLVM IR.

• HELIX focuses on the automatic translation of a class of mathematical expressions to code.
• It works by revealing implicit iteration constructs and reshaping them to match the target platform’s parallelism and vectorization capabilities.
• HELIX is rigorously defined and formally verified.
• HELIX is implemented using the Coq proof assistant.
• It supports non-linear operators.
• Presently, HELIX uses SPIRAL as an optimization oracle, but it certifies its findings.
• LLVM is used as a machine code generation backend.
• Main application: Cyber-physical systems.

Example

An application of HELIX to a real-life situation of high-assurance vehicle control (paper) using a dynamic window vehicle control approach (paper)​ is shown below:

Dependencies

• Coq
• CoLoR
• ExtLib
• math-classes
• Template Coq
• Flocq
• Vellvm (requires coq-ceres, coq-ext-lib, coq-paco, and coq-flocq) (checked out and built as a submodule)
• Jane Street Core
• coq-libhyps
• gappa + coq-gappa
• coq-dpdgraph (optional)

Clone the repository and install dependencies:

git clone --recurse-submodules https://github.com/vzaliva/helix
cd helix

To install all required dependencies:

opam repo add coq-released https://coq.inria.fr/opam/released
make -j 4 install-deps

(if some package fails to install due to missing OS dependencies, use opam depext pkgname to install the required OS packages)

To install optional dependencies:

opam install coq-dpdgraph

Building and Running

Build:

make

Run unit tests:

make test

People

• Vadim Zaliva
• Franz Franchetti
• Yannick Zakowski
• Ilia Zaichuk
• Valerii Huhnin
• Calvin Beck
• Irene Yoon
• Steve Zdancewic

HELIX was originally developed as a PhD thesis project by Vadim Zaliva under the supervision of Franz Franchetti. Ilia Zaichuk and Valerii Huhnin contributed to the proofs related to RHCOL and FHCOL compilation. Additionally, Ilia Zaichuk developed the numerical analysis module for the Dynamic Window Monitor example. Yannick Zakowski, Irene Yoon, Calvin Beck, and Steve Zdancewic performed most of the work on proving the correctness of the LLVM IR compilation pass. After completing this work, Yannick Zakowski took on the task of assembling and proving the final high-level correctness theorem.

Papers

• HELIX: From Math to Verified Code (PhD thesis)
• Modular, compositional, and executable formal semantics for LLVM IR (ICFP’21)
• Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX (VSTTE’20)
• Reification of shallow-embedded DSLs in Coq with automated verification (CoqPL’19)
• HELIX: A Case Study of a Formal Verification of High Performance Program Generation (FHPC’18)
• Formal Verification of HCOL Rewriting (FMCAD’15)

How to cite

Recommended citation:

@phdthesis{zaliva2020helix,
  title  = {{HELIX}: From Math to Verified Code},
  author = {Zaliva, Vadim},
  year   = {2020},
  school = {Carnegie Mellon University}
}

Contact

Vadim Zaliva