After the success of the last compiler social, Tobias Grosser’s research group is hosting another compiler social at the University of Cambridge’s Computer Laboratory.
Date: 05.06.2025
Time: 15 00 (Talk), 16 00 - 20 00 (Social)
Location: William Gates Building, 15 JJ Thomson Ave, Cambridge CB3 0FD 1
Rooms: LT1 (Talk), Foyer (Social)
Hosts: Emma Urquhart, Luisa Cicolini, Tobias Grosser
If you’d like to attend please make sure to register here.
There will be a talk by John Regehr at 15 00 followed by socializing in the hallway with food and drinks from 16 00 onwards.
Translation Validation for LLVM’s AArch64 Backend - John Regehr
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.