HELIX: Verified compilation of cyber-physical control systems to LLVM IR

TL;DR

HELIX is a verified code generation system that transforms high-level mathematical models of cyber-physical systems into efficient, correct LLVM IR code with formal guarantees, supporting high-performance numerical computing.

Contribution

It introduces a novel verified compilation pipeline from high-level models to LLVM IR, combining algebraic transformations and formal verification in Coq.

Findings

Successfully verified semantic preservation from high-level models to LLVM IR.

Generated efficient code for a cyber-physical robot system.

Demonstrated algebraic transformations enable parallel and vectorized processing.

Abstract

This paper presents the design of HELIX, an end-to-end verified code generation system with a focus on the intersection of high-performance and high-assurance numerical computing. The code generation can be fine-tuned to generate efficient code for a broad set of computer architectures while providing formal guarantees of the correctness of such generated code. Using a real-life example of a cyber-physical robot system, this paper demonstrates how, by using HELIX, one can start from a high-level mathematical formulation of the problem, apply a series of algebraic transformations that target intermediate languages, and generate an efficient imperative implementation. This is done while formally verifying semantic preservation from the original formulation down to LLVM IR. The method we used for high-performance code compilation is the algebraic transformation of vector and matrix computations into a dataflow optimised for parallel or vectorised processing on target hardware. The abstraction used to formalise and verify this technique is an operator language and accompanying semantics-preserving term rewriting. We use sparse vector abstraction to represent partial computations, enabling us to use algebraic reasoning to prove parallel decomposition properties. HELIX's verification infrastructure comprises multiple intermediate languages and verification approaches, all implemented in the Coq proof assistant. In particular, it uses verified term rewriting, translation validation, metaprogramming, verified compilation, layered monadic interpreters; it also supports application-specific uses of (verified) numerical analysis as we demonstrate via the running example.