llvm dev - Aug 2013 - [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