James Courtier-Dutton
2013-Aug-11 09:24 UTC
[LLVMdev] [global-isel] Simplifying the simplifier
On 10 August 2013 15:32, Nuno Lopes <nunoplopes at sapo.pt> wrote:> Hi Jakob, > > Thanks for creating this interesting proposal. > Let me just comment on this part: > > >>> What might be better is to put some abstract interface between >>> instcombine and the IR, so that instcombine can be run on these pseudo-MIs >>> as well as on IR. >> >> >> I like the idea of sharing code between IR and MI passes through an >> abstract interface. I think that later stages in the IR pipeline also need >> an instruction optimizer instead of a canonicalizer. >> >> An alternative approach would be to describe these transformations in a >> DSL instead of C++. > > >> *Legalization* >> - What does 'more legal' mean? Can we restrict the possible legalization >> transformations so the iterative process is guaranteed to make progress? > > > > I've been thinking for a while that we could express the instcombine > transformations in a DSL, and then generate the C++ code from there. The > advantage is that if we formalize the LLVM IR, then we can check the > correctness of all the instcombine transformations for "free". > Moreover, instcombine has also suffered from infinite loops in the past > (because canonicalization did not make progress for some inputs), which is > also your concern with legalization of MI. We have algorithms to prove > termination of rewriting systems, so I believe we could also prove progress > for both instcombine and MI legalization. > > I'm mixing MI legalization and instcombine, since I think that the > correctness and progress checking technology that we would need is the > exactly the same. > I wouldn't mind working on this project. But the time-frame on my side is > academic, which may mean 1 or 2 years to be completed. >Just a comment: If you believe you can represent all instcombine transformations in DSL, you then transform them to C++. Why not work out a method for checking correctness in the C++? Then, you would not have to convert everything to DSL, and could run the checks on the current C++. The code in C++ should be able to be written in a static analysis friendly way so that we could use static analysis to prove no infinite loops. James
>>>> What might be better is to put some abstract interface between >>>> instcombine and the IR, so that instcombine can be run on these >>>> pseudo-MIs >>>> as well as on IR. >>> >>> >>> I like the idea of sharing code between IR and MI passes through an >>> abstract interface. I think that later stages in the IR pipeline also >>> need >>> an instruction optimizer instead of a canonicalizer. >>> >>> An alternative approach would be to describe these transformations in a >>> DSL instead of C++. >> >> >>> *Legalization* >>> - What does 'more legal' mean? Can we restrict the possible >>> legalization >>> transformations so the iterative process is guaranteed to make progress? >> >> >> >> I've been thinking for a while that we could express the instcombine >> transformations in a DSL, and then generate the C++ code from there. The >> advantage is that if we formalize the LLVM IR, then we can check the >> correctness of all the instcombine transformations for "free". >> Moreover, instcombine has also suffered from infinite loops in the past >> (because canonicalization did not make progress for some inputs), which >> is >> also your concern with legalization of MI. We have algorithms to prove >> termination of rewriting systems, so I believe we could also prove >> progress >> for both instcombine and MI legalization. >> >> I'm mixing MI legalization and instcombine, since I think that the >> correctness and progress checking technology that we would need is the >> exactly the same. >> I wouldn't mind working on this project. But the time-frame on my side >> is >> academic, which may mean 1 or 2 years to be completed. >> > > Just a comment: > If you believe you can represent all instcombine transformations in > DSL, you then transform them to C++. > Why not work out a method for checking correctness in the C++? > Then, you would not have to convert everything to DSL, and could run > the checks on the current C++. > The code in C++ should be able to be written in a static analysis > friendly way so that we could use static analysis to prove no infinite > loops.I believe the advantage of writing down the optimizations in a DSL is that the representation is way more succinct. The code in instcombine is a bit boring and repetitive (and huge!). We could, however, try to automatically convert from C++ to the DSL. Not impossible, AFAICT. Proving absence of loops is a bit more complicated than traditional static analysis. It often requires things like synthesis of ranking functions (to prove that the transition relation is well-founded), which is not trivial. Nuni
----- Original Message -----> >>>> What might be better is to put some abstract interface between > >>>> instcombine and the IR, so that instcombine can be run on these > >>>> pseudo-MIs > >>>> as well as on IR. > >>> > >>> > >>> I like the idea of sharing code between IR and MI passes through > >>> an > >>> abstract interface. I think that later stages in the IR pipeline > >>> also > >>> need > >>> an instruction optimizer instead of a canonicalizer. > >>> > >>> An alternative approach would be to describe these > >>> transformations in a > >>> DSL instead of C++. > >> > >> > >>> *Legalization* > >>> - What does 'more legal' mean? Can we restrict the possible > >>> legalization > >>> transformations so the iterative process is guaranteed to make > >>> progress? > >> > >> > >> > >> I've been thinking for a while that we could express the > >> instcombine > >> transformations in a DSL, and then generate the C++ code from > >> there. The > >> advantage is that if we formalize the LLVM IR, then we can check > >> the > >> correctness of all the instcombine transformations for "free". > >> Moreover, instcombine has also suffered from infinite loops in the > >> past > >> (because canonicalization did not make progress for some inputs), > >> which > >> is > >> also your concern with legalization of MI. We have algorithms to > >> prove > >> termination of rewriting systems, so I believe we could also prove > >> progress > >> for both instcombine and MI legalization. > >> > >> I'm mixing MI legalization and instcombine, since I think that the > >> correctness and progress checking technology that we would need is > >> the > >> exactly the same. > >> I wouldn't mind working on this project. But the time-frame on my > >> side > >> is > >> academic, which may mean 1 or 2 years to be completed. > >> > > > > Just a comment: > > If you believe you can represent all instcombine transformations in > > DSL, you then transform them to C++. > > Why not work out a method for checking correctness in the C++? > > Then, you would not have to convert everything to DSL, and could > > run > > the checks on the current C++. > > The code in C++ should be able to be written in a static analysis > > friendly way so that we could use static analysis to prove no > > infinite > > loops. > > I believe the advantage of writing down the optimizations in a DSL is > that > the representation is way more succinct. The code in instcombine is > a bit > boring and repetitive (and huge!). > We could, however, try to automatically convert from C++ to the DSL.And, as per the purpose of the original thread ;) -- we'd like to apply the same transformation logic (or some significant part of it) both to IR and also to these global-isel pseudo-MI instructions post-legalization. -Hal> Not > impossible, AFAICT. > Proving absence of loops is a bit more complicated than traditional > static > analysis. It often requires things like synthesis of ranking > functions (to > prove that the transition relation is well-founded), which is not > trivial. > > Nuni > > _______________________________________________ > LLVM Developers mailing list > LLVMdev at cs.uiuc.edu http://llvm.cs.uiuc.edu > http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev >-- Hal Finkel Assistant Computational Scientist Leadership Computing Facility Argonne National Laboratory