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

Sign up or log in to save this to your schedule 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.


Speakers
NL

Nuno Lopes

Microsoft Research


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

Attendees (42)