Translation Validation for LLVM's AArch64 Backend

Add to your list(s) Download to your calendar using vCal

• John Regehr - University of Utah
• Thursday 05 June 2025, 15:00-16:00
• Computer Laboratory, William Gates Building, LT1.

If you have a question about this talk, please contact Luisa Cicolini.

Alive2 is a practical oracle for determining whether a transformation on LLVM IR is a refinement—that is, whether it is valid under the rules for LLVM optimizations. In this talk I’ll describe an analogous translation validation solution for LLVM ’s AArch64 backend that we’ve used to find 42 miscompilation bugs, many of which were in architecture-neutral code and hence could have also affected other backends. Our tool, arm-tv, reuses Alive2 as a source of LLVM semantics and offers a choice of two AArch64 semantics, one that we wrote by hand and the other derived from ARM ’s machine readable specification of their ISA .

John Regehr is a computer science professor at the University of Utah, USA . He liked to build tools for compiler developers to use, and then write papers about them.

If you want to attend the compiler social, please remember to sign up: https://grosser.science/compiler-social-2025-06-05/

This talk is part of the compiler socials series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Computer Architecture Group Meeting
• Computer Laboratory, William Gates Building, LT1
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• compiler socials

Note that ex-directory lists are not shown.