helix

helix copied to clipboard

• HELIX

[[https://travis-ci.com/vzaliva/helix][https://travis-ci.com/vzaliva/helix.svg?token=x87izvm44MdTPLHzuxzF&branch=master]]

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 [[http://spiral.net/][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 [[http://spiral.ece.cmu.edu:8080/pub-spiral/abstract.jsp?id=281][(paper)]] using a dynamic window vehicle control approach [[https://doi.org/10.1109/100.580977][(paper)​]] is shown below:

[[doc/bigpicture.png]]

** Dependencies

• [[https://coq.inria.fr/][Coq]]
• [[http://color.inria.fr/][CoLoR]]
• [[https://github.com/coq-ext-lib/coq-ext-lib][ExtLib]]
• [[https://github.com/math-classes/math-classes][math-classes]]
• [[https://github.com/MetaCoq/metacoq][Template Coq]]
• [[http://flocq.gforge.inria.fr/][Flocq]]
• [[https://github.com/vellvm/vellvm][Vellvm]] (requires ~coq-ceres~, ~coq-ext-lib~, ~coq-paco~, and ~coq-flocq~) /(checked out and built as a submodule)/
• [[https://opensource.janestreet.com/core/][Jane Street Core]]
• [[https://github.com/Matafou/LibHyps][coq-libhyps]]
• [[https://gitlab.inria.fr/gappa/gappa][gappa]] + [[https://gitlab.inria.fr/gappa/coq][coq-gappa]]
• [[https://github.com/Karmaki/coq-dpdgraph][coq-dpdgraph]] /(optional)/

** Clone the repository and install dependencies:

#+BEGIN_SRC sh git clone --recurse-submodules https://github.com/vzaliva/helix cd helix #+END_SRC

To install all required dependencies:

#+BEGIN_SRC sh opam repo add coq-released https://coq.inria.fr/opam/released make -j 4 install-deps #+END_SRC

(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:

#+BEGIN_SRC sh opam install coq-dpdgraph #+END_SRC

** Building and Running

*** Build:

#+BEGIN_SRC sh make #+END_SRC

*** Run unit tests:

#+BEGIN_SRC sh make test #+END_SRC

** 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 - [[https://kilthub.cmu.edu/ndownloader/files/26180729][HELIX: From Math to Verified Code (PhD thesis)]] - [[http://zaliva.org/llvm_semantics_icfp21.pdf][Modular, compositional, and executable formal semantics for LLVM IR (ICFP'21) ]] - [[http://zaliva.org/vzaliva-VSTTE20.pdf][Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX (VSTTE'20)]] - [[http://zaliva.org/vzaliva-CoqPL19.pdf][Reification of shallow-embedded DSLs in Coq with automated verification (CoqPL'19)]] - [[http://zaliva.org/vzaliva-fhpc2018.pdf][HELIX: A Case Study of a Formal Verification of High Performance Program Generation (FHPC'18)]] - [[http://zaliva.org/Formal_Verification_of_HCOL_Rewriting_FMCAD15.pdf][Formal Verification of HCOL Rewriting (FMCAD'15)]]

** How to cite Recommended citation:

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

** Contact

[[mailto:[email protected]][Vadim Zaliva]]