RSS Meetups are monthly gatherings of LASIGE members with research interests mainly in Software Architecture, Verification, Testing, Programming Languages, Type Systems, Logic, Concurrency, and Formal Methods.
Title: A Decade Verifying LLVM, or How to Retrofit Soundness in Industrial Software
Speakers: Nuno Lopes (Tecnico ULisboa)
When: April 2, 2025, 14h00
Where: FCUL, 6.3.28
Invited by: Alcides Fonseca
Abstract: LLVM is one of the most widely used compilers in the world. Its users include Apple, Google, Meta, Microsoft, PlayStation, Qualcomm, and many others. We started verifying LLVM a decade ago. In the process, we found bugs everywhere: in LLVM, in SMT solvers, in the documentation, and in our own tools. We also found shortcomings in the compiler’s theoretical models, namely of undefined behavior, memory, and concurrency. For example, we showed that it was impossible to run certain classic textbook optimizations together in LLVM. This led us to make fundamental architectural changes in LLVM itself. Moreover, LLVM keeps changing every day. We caught many regressions along the way. In this talk, we will cover our attempts to verify LLVM. The tools we built, the bugs we caught, the bugs we missed, the good and the bad surprises, and our contributions to theoretical models of compilers. We will also discuss why and how our automatic formal verification tools are used by compiler engineers on a daily basis.