HELIX

HELIX project allows for the synthesis of high-performance implementations of numerical algorithms by providing a certified compiler for formally-specified DSL. Based on the existing SPIRAL system, HELIX adds the rigor of formal verification of its correctness using the Coq proof assistant. It formally defines a series of domain-specific languages starting with HCOL, which represents a computation data flow. HELIX works by transforming the original program through a series of intermediate languages, culminating in LLVM IR.

• HELIX focuses on automatic translation a class of mathematical. expressions to code.
• It works by revealing implicit iteration constructs and re-shaping them to match target platform parallelizm and vectorization capabilities.
• HELIX is rigorously defined and formally verified.
• HELIX is implemented in Coq proof assistant.
• It supports non-linear operators.
• Presently, HELIX uses SPIRAL as an optimization oracle, but it certifies its findings.
• LLVM is used 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)

To install all required dependenceis:

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

To install optional dependencies:

opam install coq-dpdgraph

Bulding and Running

Clone the repository with submodules:

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

Build:

make

Run unit tests:

make test

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