HELIX Project: An Overview
HELIX is a formally verified language and rewriting engine for generation of high-performance implementation for a variety of numerical algorithms. 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 of 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
Development:
 |
 |
 |
 |
 |
 |
References:
- Y. Zakowski, C. Beck, I. Yoon, I. Zaichuck, V. Zaliva, S. Zdancewic
Modular, Compositional, and Executable Formal Semantics for LLVMIR
ACM SIGPLAN International Conference on Functional Programming (ICFP), 2021 - Y. Zakowski
[POPL 2021] CoqPL: Verifying a Compiler Through Equational Means
Symposium on Principles of Programming Languages (POPL), 2021, presentation - V. Zaliva, I. Zaichuk, F. Franchetti
Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX
12th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2020 - V. Zaliva, M. Sozeau
Reification of Shallow-Embedded DSLs in Coq with Automated Verification
International Workshop on Coq for Programming Languages (CoqPL), 2019 - V. Zaliva, F. Franchetti
HELIX: A Case Study of a Formal Verification of High Performance Program Generation
Workshop on Functional High Performance Computing (FHPC), 2018 [video of presentation] - V. Zaliva, F. Franchetti
Reasoning About Sparse Vectors for Loops Code Generation
ACM SIGPLAN International Conference on Functional Programming (ICFP), 2017, poster - V. Zaliva, F. Franchetti
Formal Verification of HCOL Rewriting
Formal Methods in Computer-Aided Design (FMCAD), 2015 - V. Zaliva, F. Franchetti
Formal Verification of HCOL Rewriting
Formal Methods in Computer-Aided Design (FMCAD), 2015, poster
For more information, visit the HELIX GitHub repository.
Copyrights to many of the above papers are held by the publishers. The attached PDF 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. Some links to papers above connect to IEEE Xplore with permission from IEEE, and viewers must follow all of IEEE's copyright policies.