Translation Validation for LLVM's 64-bit RISC-V and ARM Backends
Details
John Regehr from University of Utah will give a seminar on:
Translation Validation for LLVM's 64-bit RISC-V and ARM Backends
This event is in person.
🗓 Date & Time: Thursday, October 8, 2026, at 16:00
📍 Location: Room 1440 Henrik Eriksson, KTH
Abstract
LLVM's backends translate its intermediate representation to assembly or
object code. In effect, these compiler backends are highly optimizing
compilers in their own right, and they contain bugs. As a step towards
gaining confidence in the correctness of work done by LLVM backends, we
have created arm-tv and riscv-tv, which formally verify translations
between LLVM IR and 64-bit ARM and RISC-V code. Ours is not the first
translation validation work for LLVM, but we have advanced the state of
the art along multiple fronts: we enforce various ABI rules; we have
extended Alive2 (which we reuse as a verification backend) to deal with
unstructured mixes of pointers and integers that are typical of assembly
code; we investigate the tradeoffs between hand-written AArch64
semantics and those derived mechanically from ARM's published formal
semantics; and, we have discovered 46 previously unknown miscompilation
bugs in LLVM backends many of which affected multiple targets and most
of which are now fixed in upstream LLVM.
About the speaker
John Regehr has been on the computer science faculty at the University
of Utah since 2003. All of his recent work is on making compilers less
buggy, easier to engineer, and more highly optimizing. When not working,
he tries to spend as much time as possible outdoors.
Webpage: https://john.regehr.org/