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.<br><br><div class="gmail_quote">
On Fri, Apr 8, 2011 at 6:04 AM, Duncan Sands <span dir="ltr"><<a href="mailto:baldrick@free.fr">baldrick@free.fr</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi Rafael, don't forget to submit your proposal to GSOC (via the GSOC web-page)<br>
- the deadline is today!<br>
<div><div></div><div class="h5"><br>
><br>
>     It sounds like you are planning to follow the approach of Joshi, Nelson and<br>
>     Randall ("Denali: A Goal-directed Superoptimizer") in that you don't intend<br>
>     to exhaustively enumerate all possible code sequences, and see if they are<br>
>     the same as the original only better; but instead start from the original code<br>
>     sequence and repeatedly apply transformations that change code to equivalent<br>
>     code, looking to see if you can eventually get something better than the<br>
>     original.  Is that right?<br>
><br>
><br>
> Exactly. If we can use axioms/transformations/identities which don't modify the<br>
> code behavior, but just tries to interpret instruction semantics in a different<br>
> way, so as to find another (and hopefully simpler) instructions to do the same<br>
> job, the role of the SAT prover is no longer necessary, since the search space<br>
> is constrained to expressions which are semantically equivalent.<br>
><br>
> Example:<br>
> Transformation:  (ADD  Operand_A, Contant 0) <- equivalent to-> Operand_A<br>
><br>
> Using this transformation, the search algorithm now can simplify "add A with 0"<br>
> to "A" or, what may look initially not so useful, transform any operand A into<br>
> an add with A plus 0. Later, this is important to prove we can use an add<br>
> instruction to load any operand. Well, I think you got the idea of using a set<br>
> of axioms... this, in practice, is important to prove an arbitrary sequence A is<br>
> equivalent to SequenceB, and, if B is shorter than A, use B instead.  Speaking<br>
> of implementation, there will be a big list of transformations and a "for" loop<br>
> trying each transformation and recursively applying more transformations, until<br>
> we can show a code sequence is equivalent to another. This is a short overview<br>
> of the algorithm and how I worked in this area. If you prefer another approach<br>
> described formally in another paper, I can study it and use another algorithm.<br>
<br>
</div></div>I am fine with this approach, even though it can miss interesting reductions,<br>
since it is way more efficient (from what I hear) than the fully general<br>
approach, so should be able to handle code sequences longer than just a couple<br>
of instructions.<br>
<div><div></div><div class="h5"><br>
Ciao, Duncan.<br>
_______________________________________________<br>
LLVM Developers mailing list<br>
<a href="mailto:LLVMdev@cs.uiuc.edu">LLVMdev@cs.uiuc.edu</a>         <a href="http://llvm.cs.uiuc.edu" target="_blank">http://llvm.cs.uiuc.edu</a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev</a><br>
</div></div></blockquote></div><br>