llvm dev - Aug 2013 - [LLVMdev] [global-isel] Simplifying the simplifier

On Aug 10, 2013, at 7:32 AM, Nuno Lopes <nunoplopes at sapo.pt> wrote:
>> 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.
This sounds promising. But we have some requirements that textbook rewriting
systems can't handle:

- Expressions are DAGs, not trees.
- Targets can add custom rewriting rules and override standard rules.
- Rules will have predicates. Some predicates are static and only depend on the
subtarget, some predicates will depend on the pattern being matched.
- The system won't be convergent if you ignore all the predicates.

So the question is, given those requirements, can we still prove termination?

Thanks,
/jakob

>>> 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.
>
> This sounds promising. But we have some requirements that textbook 
> rewriting systems can't handle:
>
> - Expressions are DAGs, not trees.
> - Targets can add custom rewriting rules and override standard rules.
> - Rules will have predicates. Some predicates are static and only depend 
> on the subtarget, some predicates will depend on the pattern being 
> matched.
> - The system won't be convergent if you ignore all the predicates.
>
> So the question is, given those requirements, can we still prove 
> termination?
Uhm, I'm not sure about the custom target rules, since most likely a bunch 
of them will need to be specified in C++, and then they will be a black box 
to the tool..

Regarding the predicates, how complicated are these?  Aren't these 
expressions mostly in linear integer arithmetic?  Or can you have arbitrary 
calls to complex C++ code?

Nuno

On Aug 11, 2013, at 4:14 AM, "Nuno Lopes" <nunoplopes at
sapo.pt> wrote:
>> This sounds promising. But we have some requirements that textbook
rewriting systems can't handle:
>> 
>> - Expressions are DAGs, not trees.
>> - Targets can add custom rewriting rules and override standard rules.
>> - Rules will have predicates. Some predicates are static and only
depend on the subtarget, some predicates will depend on the pattern being
matched.
>> - The system won't be convergent if you ignore all the predicates.
>> 
>> So the question is, given those requirements, can we still prove
termination?
> 
> Uhm, I'm not sure about the custom target rules, since most likely a
bunch of them will need to be specified in C++, and then they will be a black
box to the tool..
I think that SelectionDAG forces you to drop to C++ too soon, but we'll
always need that possibility.
> Regarding the predicates, how complicated are these?  Aren't these
expressions mostly in linear integer arithmetic?  Or can you have arbitrary
calls to complex C++ code?
There are too many static predicates, so it isn't feasible to enumerate all
possible combinations, but we can expose their relationships to the tool as
boolean expressions. For example, X86 currently has:

def HasCMov      : Predicate<"Subtarget->hasCMov()">;
def NoCMov       : Predicate<"!Subtarget->hasCMov()">;

It would be simple to define:

def NoCMov       : Predicate<(not HasCMov)>;

And the tool would be able to infer that the predicates are disjoint. Similarly:

def : Always<(or HasSSE1, (not HasSSE2))>;

can be used to infer an implication.

Many pattern predicates could be expressed in a DSL, but we should still make it
possible to use C++ code.

Thanks,
/jakob

-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20130811/e91c18b2/attachment.html>