Invited Speakers 

The Impossible Quest of Verifying the LLVM Ecosystem

Compilers are the core of our software ecosystem. Yet, maintaining proofs of their formal correctness conflicts with the need for fast evolution of our compiler stacks. Programming languages such as C++, Rust, Julia, and Lean utilize LLVM as their backend, and LLVM’s MLIR project extends LLVM technology to hardware design, cryptography, quantum computing, and the current AI software stack. Fast evolution is key to delivering peak performance for the latest workloads. Hence, streamlined software development is a must. Slowdowns, e.g., for additional formal reasoning, are undesirable. We ask: how can we bring formal methods to such a complex compiler ecosystem? We discuss the state of formal verification in the LLVM ecosystem and share our work towards bringing formal verification to MLIR-based compilers. As a first step, we introduce SMT-level abstractions as first-class verification dialects to MLIR. We then look at recent efforts to verify peephole optimizations at scale using the Lean ITP, detailing our work on bitvector reasoning and the development of relevant decision procedures. After reporting on our recent work on bringing authoritative RISC-V semantics, we discuss future steps to further increase formal reasoning in LLVM.

Tobias Grosser is an Associate Professor at the University of Cambridge. Before, he worked as a Reader at the University of Cambridge, as an Ambizione Fellow at ETH Zurich, and as a Google PhD Fellow at INRIA/Paris IV/ENS Paris. Tobias and his research group have a decade-long history of contributing to the LLVM ecosystem. Tobias developed polyhedral loop optimizations in LLVM/Polly, worked on hardware design with LLHD/CIRCT, and developed the xDSL Python-Native MLIR-style compiler framework. Over the last years, he started to look into formal methods in the context of the Lean ITP.