You are viewing a plain text version of this content. The canonical link for it is here.
Posted to commits@tvm.apache.org by GitBox <gi...@apache.org> on 2022/01/15 15:22:29 UTC
[GitHub] [tvm] wrongtest opened a new pull request #9941: [TIR] Canonical simplify the intset before region cover proof
wrongtest opened a new pull request #9941:
URL: https://github.com/apache/tvm/pull/9941
Hi, this is a simple modification for region cover check, which I believe can fix the region cover failure of https://github.com/apache/tvm/pull/9527.
However, I believe it could not eliminate all possible failures to prove the region cover property. Why the case of https://github.com/apache/tvm/pull/9527 can be fixed is described below:
1. Originally, for h-axis, the produced region's max is:
- `(((1 + ((min((225 - (hh_0*8)), 10) - max((1 - (hh_0*8)), 0)) - 1)) + (((hh_0*8) - 1) + max((1 - (hh_0*8)), 0))) - 1)`
2. Human can quickly find a `a + b - b => a` pattern to simplify, and so with `canonical_simplify`:
- `(((hh_0*8) + (225 - max((hh_0*8), 215))) - 2)`
3. However, `analyzer.Simplify()`, specially, in it's invocation to `rewrite_simplify`, the original expr is transform to
- `((((225 - max((hh_0*8), 215)) + max((hh_0*8), 1)) - max((1 - (hh_0*8)), 0)) - 2)`
4. The form in (3) is too complex to be proved to cover the consumer region.
5. So try manually call `canonical_simplify` before any general simplification (`analyzer.Simplify` is invoked in many places, for example, in a intset intersection call) works for this particular problem.
6. Since `CanProve` interface also invoke simplifications, actually we do not need to manually call `analyzer.Simplify` twice.
So the root cause should be rule conflictions in `canonical_simplify` and `rewrite_simplify`, and `analyzer.Simplify` will always use `rewrite_simplify` first. The pr is not aimed to resolve this general issue.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] Hzfengsy merged pull request #9941: [TIR] Canonical simplify the intset before region cover proof
Posted by GitBox <gi...@apache.org>.
Hzfengsy merged pull request #9941:
URL: https://github.com/apache/tvm/pull/9941
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] tqchen commented on pull request #9941: [TIR] Canonical simplify the intset before region cover proof
Posted by GitBox <gi...@apache.org>.
tqchen commented on pull request #9941:
URL: https://github.com/apache/tvm/pull/9941#issuecomment-1016884151
Great discussions. The min/max cancelation was not a topic that come up before but indeed worth thinking a bit more.
- The specific match to cancel is a good middle ground because the rule only triggers for the specific case and we know it is useful. (so this is the change that would be net positive with minimum impact)
- As a followup step, would love to have more indepth thinking about canonical form and how can they affect the cancelation, as @wrongtest suggested
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] wrongtest commented on a change in pull request #9941: [TIR] Canonical simplify the intset before region cover proof
Posted by GitBox <gi...@apache.org>.
wrongtest commented on a change in pull request #9941:
URL: https://github.com/apache/tvm/pull/9941#discussion_r787265041
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -153,6 +153,16 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const AddNode* op) {
TVM_TRY_REWRITE(max(x, y - z) + z, max(x + z, y));
TVM_TRY_REWRITE(max(x - z, y) + z, max(x, y + z));
+ TVM_TRY_REWRITE(min(c1, x - c2) + c3, min(c1 + c3, x + (c3 - c2)));
Review comment:
Background: after process region only use `canonical_simplify` and intersect with buffer shape bound, the region max to compare now are (after https://github.com/apache/tvm/pull/9880). The issue is to cancel `hh_0*8` in min.
- `min(0, ((hh_0*8) - 215)) + 223)`
- `min(((hh_0*8) + 9), 224) - 1)`
My thought for the rule is it would do reduce the expression depth, because `c1`, `c2`, `c3` are `PVar<IntImm>` and get immediately folded. Other possible rule replacements I can imagine could be:
- (make min to a "canonical" form) `min(c1, x-c2)` => `min(0, x-(c1+c2)) + c1`
- (specifically match things to cancel) `min(c1, x-c2) - min(c3, x-c4)` => 0 if c1+c2=c3+c4
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] junrushao1994 commented on pull request #9941: [TIR] Canonical simplify the intset before region cover proof
Posted by GitBox <gi...@apache.org>.
junrushao1994 commented on pull request #9941:
URL: https://github.com/apache/tvm/pull/9941#issuecomment-1013726746
I will leave @Hzfengsy to coordinate the change
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] wrongtest commented on pull request #9941: [TIR] Canonical simplify the intset before region cover proof
Posted by GitBox <gi...@apache.org>.
wrongtest commented on pull request #9941:
URL: https://github.com/apache/tvm/pull/9941#issuecomment-1025154111
Finally I found there are existing rules can cover pattern like `min(c1, x-c2) - min(c3, x-c4) => c4-c2`, so there is no need to add more rules for my requirement.
> https://github.com/apache/tvm/blob/main/src/arith/rewrite_simplify.cc#L307-L315
However, to make these rules work, I have to call `canonical_simplify` again, to move the terms which can be cancelled together. cc @spectrometerHBH @Hzfengsy would you kindly review it again? I believe then I can turn back to pending compute_at issue of #9527.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] wrongtest commented on a change in pull request #9941: [TIR] Canonical simplify the intset before region cover proof
Posted by GitBox <gi...@apache.org>.
wrongtest commented on a change in pull request #9941:
URL: https://github.com/apache/tvm/pull/9941#discussion_r787265041
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -153,6 +153,16 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const AddNode* op) {
TVM_TRY_REWRITE(max(x, y - z) + z, max(x + z, y));
TVM_TRY_REWRITE(max(x - z, y) + z, max(x, y + z));
+ TVM_TRY_REWRITE(min(c1, x - c2) + c3, min(c1 + c3, x + (c3 - c2)));
Review comment:
Background: after process region only use `canonical_simplify` and intersect with buffer shape bound, the region max to compare now are (after https://github.com/apache/tvm/pull/9880). The issue is to cancel `hh_0*8` in min.
- `min(0, ((hh_0*8) - 215)) + 223)`
- `min(((hh_0*8) + 9), 224) - 1)`
My thought for the rule is it would do reduce the expression depth, because `c1`, `c2`, `c3` are `PVar<IntImm>` and get immediately folded. Other possible rule replacements I can imagine could be:
- (make min to a "canonical" form) `min(c1, x-c2)` => `min(0, x-(c1+c2)) + c1`
- (specifically match things to cancel) `min(c1, x-c2) - min(c3, x-c4)` => c4-c2 if c1+c2=c3+c4
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] spectrometerHBH commented on a change in pull request #9941: [TIR] Canonical simplify the intset before region cover proof
Posted by GitBox <gi...@apache.org>.
spectrometerHBH commented on a change in pull request #9941:
URL: https://github.com/apache/tvm/pull/9941#discussion_r787013464
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -153,6 +153,16 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const AddNode* op) {
TVM_TRY_REWRITE(max(x, y - z) + z, max(x + z, y));
TVM_TRY_REWRITE(max(x - z, y) + z, max(x, y + z));
+ TVM_TRY_REWRITE(min(c1, x - c2) + c3, min(c1 + c3, x + (c3 - c2)));
Review comment:
These rules look quite ad-hoc to me since in general, I think it would be more simplified to keep common sub expressions out of min/max to avoid duplicate calculation unless it can cancel some items like the rules above `max(x-z, y) + z, max(x, y+z)`.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] wrongtest commented on pull request #9941: [TIR] Canonical simplify the intset before region cover proof
Posted by GitBox <gi...@apache.org>.
wrongtest commented on pull request #9941:
URL: https://github.com/apache/tvm/pull/9941#issuecomment-1015980480
Also I have question on whether there are solid ways to avoid patch codes at all. For example, can we prefer to cancel all common terms in summation before any other rewrites?
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] Hzfengsy commented on pull request #9941: [TIR] Canonical simplify the intset before region cover proof
Posted by GitBox <gi...@apache.org>.
Hzfengsy commented on pull request #9941:
URL: https://github.com/apache/tvm/pull/9941#issuecomment-1014229280
ping @spectrometerHBH
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] wrongtest commented on pull request #9941: [TIR] Canonical simplify the intset before region cover proof
Posted by GitBox <gi...@apache.org>.
wrongtest commented on pull request #9941:
URL: https://github.com/apache/tvm/pull/9941#issuecomment-1013699716
cc @Hzfengsy @spectrometerHBH
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] spectrometerHBH commented on a change in pull request #9941: [TIR] Canonical simplify the intset before region cover proof
Posted by GitBox <gi...@apache.org>.
spectrometerHBH commented on a change in pull request #9941:
URL: https://github.com/apache/tvm/pull/9941#discussion_r787013464
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -153,6 +153,16 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const AddNode* op) {
TVM_TRY_REWRITE(max(x, y - z) + z, max(x + z, y));
TVM_TRY_REWRITE(max(x - z, y) + z, max(x, y + z));
+ TVM_TRY_REWRITE(min(c1, x - c2) + c3, min(c1 + c3, x + (c3 - c2)));
Review comment:
These rules look quite ad-hoc to me since in general, I think it would be great to keep common sub expressions out of min/max to avoid duplicate calculation unless it can cancel some items like the rules above `max(x-z, y) + z, max(x, y+z)`.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org
For queries about this service, please contact Infrastructure at:
users@infra.apache.org