LLVM M.D.A Denotational Translation Validator |
 |
LLVM M.D. (Mis-optimization Detector) is a compiler research project at
Harvard University.
Our goal is to detect when a compiler optimization changes the meaning
of the input program. This almost always indicates a bug in the optimizer.
For our project we are using the LLVM
optimization framework.
Our tools work by analysing two LLVM programs and trying to determine
if they have the same meaning. Our tools do not require any integration
with the optimizer to work, and can also be used on hand-optimized code.
This technique is called "Translation Validation", and our work is focused
around scaling this technique to a real-world compiler such as LLVM.
We hope that our tools will be useful for compiler developers, and for
industries where safety-critical software is important and optimization is
needed.
Recent News
February 7, 2011: New Paper Available
A new paper describing LLVM M.D. has been accepted for publication. A
draft of the paper is available under "Publications".
February 7, 2011: Updated Source Code
We have released the source code for the version of our tool used to
generate data for our PLDI submission. This version will not be supported
as we are continuing to make changes and improvements.
September 8, 2010: Updated Experimental Results
Improved and expanded experimental results have been posted using the
newest version of LLVM-MD. Please see the Experimental Results section
for more information.
September 7, 2010: New Version
A new version of LLVM-MD is now available. This version incorporates a
alternative to structural analysis for identifying program structure, and
is able to handle more functions, with a lower false alarm rate.
July 15, 2010: New Research Paper
We have posted our first research paper related to our tools:
LLVM M.D.: A Denotational Translation Validator. Please see the
Publications section for more information.