[LLVMdev] GSoC 2011: Superoptimization for LLVM IR

[Rafael Auler]

Ok, I've submitted now a revised version considering all these valuable
comments about the project. I hope to contribute to the LLVM community as
much as the LLVM project contributed to my thesis. Thanks.

On Fri, Apr 8, 2011 at 6:04 AM, Duncan Sands <baldrick at free.fr> wrote:

> Hi Rafael, don't forget to submit your proposal to GSOC (via the GSOC
> web-page)
> - the deadline is today!
>
> >
> >     It sounds like you are planning to follow the approach of Joshi,
> Nelson and
> >     Randall ("Denali: A Goal-directed Superoptimizer") in that you don't
> intend
> >     to exhaustively enumerate all possible code sequences, and see if
> they are
> >     the same as the original only better; but instead start from the
> original code
> >     sequence and repeatedly apply transformations that change code to
> equivalent
> >     code, looking to see if you can eventually get something better than
> the
> >     original.  Is that right?
> >
> >
> > Exactly. If we can use axioms/transformations/identities which don't
> modify the
> > code behavior, but just tries to interpret instruction semantics in a
> different
> > way, so as to find another (and hopefully simpler) instructions to do the
> same
> > job, the role of the SAT prover is no longer necessary, since the search
> space
> > is constrained to expressions which are semantically equivalent.
> >
> > Example:
> > Transformation:  (ADD  Operand_A, Contant 0) <- equivalent to-> Operand_A
> >
> > Using this transformation, the search algorithm now can simplify "add A
> with 0"
> > to "A" or, what may look initially not so useful, transform any operand A
> into
> > an add with A plus 0. Later, this is important to prove we can use an add
> > instruction to load any operand. Well, I think you got the idea of using
> a set
> > of axioms... this, in practice, is important to prove an arbitrary
> sequence A is
> > equivalent to SequenceB, and, if B is shorter than A, use B instead.
>  Speaking
> > of implementation, there will be a big list of transformations and a
> "for" loop
> > trying each transformation and recursively applying more transformations,
> until
> > we can show a code sequence is equivalent to another. This is a short
> overview
> > of the algorithm and how I worked in this area. If you prefer another
> approach
> > described formally in another paper, I can study it and use another
> algorithm.
>
> I am fine with this approach, even though it can miss interesting
> reductions,
> since it is way more efficient (from what I hear) than the fully general
> approach, so should be able to handle code sequences longer than just a
> couple
> of instructions.
>
> Ciao, Duncan.
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20110408/eb7ce413/attachment.html>