For full conference details, see the website: http://llvm.org/devmtg/2019-10/
Back To Schedule
Wednesday, October 23 • 5:00pm - 5:35pm
Alive2: Verifying Existing Optimizations

Sign up or log in to save this to your schedule, view media, leave feedback and see who's attending!

Alive is regularly used to verify InstCombine optimizations. However, it is limited mostly to InstCombine-style optimizations, and it can only verify optimizations written in Alive's own IR-like DSL.

Alive2 is a re-implementation of Alive that removes several limitations of the previous tool. It supports floating point operations and has better support for memory and loops. It handles optimizations beyond those found in InstCombine. It includes a standalone tool that can prove equivalence / refinement between two bitcode functions as well as an `opt` plugin that can prove that an LLVM optimization is correct. Neither of these new tools requires optimizations to be rewritten in the Alive DSL.

In this talk, we will give an overview on Alive2 and show how you can use it to 1) ensure your optimization is correct, and 2) to find that bug that is triggering a miscompilation.


Nuno Lopes

Microsoft Research

Wednesday October 23, 2019 5:00pm - 5:35pm PDT
General Session (LL20ABC)