[ARITH] Improve div/mod in rewrite simplifier #3149

sgrechanik-h · 2019-05-08T14:04:59Z

This PR improves division-related rewriting rules.

tqchen · 2019-05-08T15:22:18Z

Thanks for the PR. One thing I want to note is that we want to focus on the good use-cases in index simplification.

Think about specific index simplification applications
Collectively use rewrite/canonical simplifier

For example, it is a bit unclear whether taking the gcd out from x * c1 + y * c2 is helpful in a particular case(the canonical does it in another way). Similarly, most of the divisions we encounter in index simplification will rarely have a negative value in the right operand.

To elaborate about the second principle, given that canonical simplifier now inheritates rewrite simplifier, we might be able to use canonical for many cases that rewrite simplifier is not good at.

It would be great if we can provide some justifications for the set of changes.

include/tvm/arithmetic.h

sgrechanik-h · 2019-05-08T17:02:26Z

@tqchen I'm currently trying to move my implementation of tensor expression autodiff to the new simplifiers instead of the obsolete Halide simplifier. Most of these changes are required for simplifying complex automatically generated expressions involving divisions. Most of the new rules are just slightly modified copies of the existing rules, just to cover more cases.

For example, it is a bit unclear whether taking the gcd out from x * c1 + y * c2 is helpful in a particular case(the canonical does it in another way).

It is needed to simplify expressions like 2 * x + 4 * y <= 0. I think I can move it to the LT case.

Similarly, most of the divisions we encounter in index simplification will rarely have a negative value in the right operand.

I can remove the corresponding test cases and the rules specifically designed to cover the negative divisor case, since they are not really required by the autodiff. However I would keep them just in case.

To elaborate about the second principle, given that canonical simplifier now inheritates rewrite simplifier, we might be able to use canonical for many cases that rewrite simplifier is not good at.

The rewrite simplifier has a clear design, so I would prefer fixing the rewrite simplifier rather than the canonical simplifier.

Currently there are CI errors which seem to be connected to the fact that the old Halide notion of division is still in use in some parts of TVM. I didn't expect it and have to think what to do with them.

tqchen · 2019-05-08T17:14:44Z

I see, thanks for sharing your thoughts! I agree with most of your comment. I do hope that we can move forward to have a combined use case of canonical/rewrite simplifications. Given that canonical can be much more global and will be our default simplifier in the future.

Specifically, the canonical simplifier can aggressively simplify complicated patterns of div/mod which are otherwise hard for rewrite simplifier

tqchen · 2019-05-11T00:27:03Z

@sgrechanik-h after some thoughts i think we can bring these changes in as long as they are properly reviewed. Can you tag more reviewers and address the CI issue? Thanks!

sgrechanik-h · 2019-05-11T06:38:57Z

@tqchen Sure. I want to run some additional tests though, so I will do it around monday.

sgrechanik-h · 2019-05-13T18:30:03Z

The tests were failing because I enabled const folding when dividing negative numbers. Some parts of tvm (like the bound deducer) still assume that the division is euclidean, and since they also use const folding, enabling it for negative numbers (using truncated division) breaks them. Such parts should be rewritten or removed in the future, because currently they may lead to incorrect code. For now I just added additional const folding rule in the rewrite simplifier (which is not used in legacy code, hopefully).

@derisavi @merrymercy @kazum @wweic Please review

wweic

lgtm.

src/arithmetic/modular_set.h

derisavi · 2019-05-15T01:44:37Z

src/arithmetic/rewrite_simplify.cc

-                       CanProveGreaterEqual(x.Eval(), 0) && c1.Eval()->value > 0);
+                       c1.Eval()->value != 0);
+    TVM_TRY_REWRITE_IF(x - ((x + c2) / c1) * c1, (x + c2) % c1 - c2,
+                       c1.Eval()->value != 0);


if we replace c2 by y (a non-const), would the rule still be correct?

It should be. I'll fix it and add more tests.

derisavi · 2019-05-15T01:53:17Z

src/arithmetic/rewrite_simplify.cc

+        auto pgcd = PConstWithTypeLike<PVar<Expr>>(x, gcd);
+        return ((x * b1 + y * b2) * pgcd).Eval();
+      }
+    }


I have the same question as Tianqi. I read your answer as follows:

It is needed to simplify expressions like 2 * x + 4 * y <= 0. I think I can move it to the LT case.

But still didn't quite understand what you mean. Do you mean that from 2x + 4y <= 0, we can derive x + 2*y <= 0? Can you elaborate please?

Do you mean that from 2x + 4y <= 0, we can derive x + 2*y <= 0?

Yes, exactly.

What I don't understand is how dealing with x+2y <= 0 is any better/easier/simpler than 2x+4y <= 0?

Ok, I decided to investigate, and turned out I was wrong, and the rule is beneficial for a different reason, namely it transforms x*3 - (x/2)*6 into (x - (x/2)*2)*3 which is then transformed into (x % 2) * 3 by another rule (the resulting expression is easier for bound analysis).

I think, It is possible to replace this rule with a bunch of more specialized rules, however I would prefer a more general rule.

Does it make sense to do the simplification if c1 (resp. c2) is divisible by c2 (resp. c1)?

Even if it does, I still can't convince myself that xc1 + yc2 -> (x+yc3)c1 (where c3 = c2/c1) is always a beneficial transformation. For example, consider (6x + 3y) - (6y + 2z). If we simplify each parenthesized expression first and get 3*(2x+y) - 2(3*y+z), we may not be able to simplify further. I just see the problem but not a solution in my suggestion.

(6x + 3y) - (6y + 2z) cannot be simplified by the rewrite simplifier anyway. And the canonical simplifier is able to simplify both it and 3*(2x+y) - 2(3*y+z). However, this is indeed controversial, so I'll disable the transformation, and may be add several special-case rules instead.

sgrechanik-h · 2019-05-17T13:28:57Z

I replaced the GCD rule with several more specialized rules. Please rereview.

tqchen · 2019-05-17T17:08:31Z

await further comments from @derisavi , @kazum please take a look if you have time

huajsj · 2019-05-19T20:30:12Z

src/arithmetic/rewrite_simplify.cc

@@ -99,6 +93,12 @@ TryCompare(const Expr& x, int64_t val) {
  if (dbound->max_value <= val) {


for enhancement , do we need to change dbound->max_value <= val into dbound->max_value == val? similar existing issue in line 90.

I'm not sure this is really an enhancement, current formulation seems more straightforward, e.g. if max_value were an Expr, we could write can_prove(max_value <= val) whereas can_prove(max_value == val) would be "less complete".

derisavi · 2019-05-21T19:51:49Z

src/arithmetic/rewrite_simplify.cc

+    TVM_TRY_REWRITE_IF(((x - y) / c1) * c3 - x * c2, ((y - x) % c1 - y) * c2,
+                       c1.Eval()->value != 0 &&
+                       c3.Eval()->value == c1.Eval()->value * c2.Eval()->value);
+


The rules are all correct to me. Thanks.
What happens if we have something like c2 * x - c3 * (x / c1) ( I used commutativity) ? Does the simplifier automatically use TVM_TRY_RECURSIVE_REWRITE(c1 * x, x * c1); in its attempt to simplify it?

Yes, this particular example works thanks to this canonicalization rule. I've added a couple of tests to be sure.

derisavi · 2019-05-21T19:55:31Z

src/arithmetic/rewrite_simplify.cc

+      int64_t c2val = c2.Eval()->value;
+      return make_const(op->type, c1val / c2val);
+    }
+


derisavi · 2019-05-21T20:19:29Z

src/arithmetic/rewrite_simplify.cc

-    TVM_TRY_REWRITE_IF(x / c1 < c2, x < c1 * c2,
-                       c1.Eval()->value > 0 &&
+    TVM_TRY_REWRITE_IF(x * c2 < c1, x < c1 / c2,
+                       c1.Eval()->value <= 0 &&
                       c2.Eval()->value > 0);


This is true if x is an integer. Can we assume that?

I think we can, since these rules are guarded by the condition IsIndexType(op->a.type()), and also all constants are declared as integers (PVar<Integer>).

derisavi · 2019-05-21T21:08:25Z

Other than the comments above, it LGTM.

tqchen · 2019-05-24T16:58:13Z

src/arithmetic/rewrite_simplify.cc

+                       c1.Eval()->value != 0 &&
+                       c3.Eval()->value == c1.Eval()->value * c2.Eval()->value);
+    TVM_TRY_REWRITE_IF(((x - y) / c1) * c3 - x * c2, ((y - x) % c1 - y) * c2,
+                       c1.Eval()->value != 0 &&


@sgrechanik-h please update the comment to mark all the cases that require special truc div rule. So we can be sure about this later

// NOTE: trunc div required

Co-Authored-By: Wei Chen <[email protected]>

derisavi

LGTM. Thanks @sgrechanik-h.

tqchen · 2019-05-27T16:33:08Z

Thanks, @sgrechanik-h @wweic @derisavi @huajsj . This PR is now merged

* [ARITH] Improve div/mod in rewrite simplifier * Fix lint error * Fuller file name in src/arithmetic/modular_set.h Co-Authored-By: Wei Chen <[email protected]> * Generalize some rules * Replace gcd factoring with specialized rules * Mark rules that don't work for non-truncated division * More tests

tqchen self-assigned this May 8, 2019

tqchen requested changes May 8, 2019

View reviewed changes

include/tvm/arithmetic.h Outdated Show resolved Hide resolved

tqchen added the status: need update need update based on feedbacks label May 8, 2019

sgrechanik-h force-pushed the pr-rw-divmod-improvements branch from ea6ba99 to 52cfa09 Compare May 13, 2019 12:06

tqchen added the status: need review label May 13, 2019

wweic approved these changes May 14, 2019

View reviewed changes

src/arithmetic/modular_set.h Outdated Show resolved Hide resolved

derisavi reviewed May 15, 2019

View reviewed changes

huajsj reviewed May 19, 2019

View reviewed changes

derisavi reviewed May 21, 2019

View reviewed changes

tqchen approved these changes May 24, 2019

View reviewed changes

tqchen requested changes May 24, 2019

View reviewed changes

sgrechanik-h and others added 5 commits May 27, 2019 11:25

[ARITH] Improve div/mod in rewrite simplifier

0251237

Fix lint error

150b110

Fuller file name in src/arithmetic/modular_set.h

46a6ded

Co-Authored-By: Wei Chen <[email protected]>

Generalize some rules

b665deb

Replace gcd factoring with specialized rules

17b47ac

sgrechanik-h force-pushed the pr-rw-divmod-improvements branch from 98d0663 to f14aa9a Compare May 27, 2019 11:02

sgrechanik-h added 2 commits May 27, 2019 14:04

Mark rules that don't work for non-truncated division

f14aa9a

More tests

978ae69

derisavi approved these changes May 27, 2019

View reviewed changes

tqchen removed the status: need review label May 27, 2019

tqchen added status: accepted and removed status: need update need update based on feedbacks labels May 27, 2019

tqchen approved these changes May 27, 2019

View reviewed changes

tqchen merged commit 8814ada into apache:master May 27, 2019

sgrechanik-h deleted the pr-rw-divmod-improvements branch November 3, 2019 17:52

tqchen mentioned this pull request Nov 8, 2019

[RELEASE][DRAFT] TVM v0.6 Release candidate #4259

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[ARITH] Improve div/mod in rewrite simplifier #3149

[ARITH] Improve div/mod in rewrite simplifier #3149

sgrechanik-h commented May 8, 2019

tqchen commented May 8, 2019

sgrechanik-h commented May 8, 2019

tqchen commented May 8, 2019 •

edited

Loading

tqchen commented May 11, 2019

sgrechanik-h commented May 11, 2019

sgrechanik-h commented May 13, 2019

wweic left a comment

derisavi May 15, 2019

sgrechanik-h May 15, 2019

derisavi May 15, 2019

sgrechanik-h May 15, 2019

derisavi May 15, 2019

sgrechanik-h May 16, 2019

derisavi May 16, 2019

sgrechanik-h May 16, 2019

sgrechanik-h commented May 17, 2019

tqchen commented May 17, 2019

huajsj May 19, 2019

sgrechanik-h May 20, 2019

derisavi May 21, 2019

sgrechanik-h May 27, 2019

derisavi May 21, 2019

derisavi May 21, 2019

sgrechanik-h May 27, 2019

derisavi commented May 21, 2019

tqchen May 24, 2019

derisavi left a comment

tqchen commented May 27, 2019

		@@ -99,6 +93,12 @@ TryCompare(const Expr& x, int64_t val) {
		if (dbound->max_value <= val) {

[ARITH] Improve div/mod in rewrite simplifier #3149

[ARITH] Improve div/mod in rewrite simplifier #3149

Conversation

sgrechanik-h commented May 8, 2019

tqchen commented May 8, 2019

sgrechanik-h commented May 8, 2019

tqchen commented May 8, 2019 • edited Loading

tqchen commented May 11, 2019

sgrechanik-h commented May 11, 2019

sgrechanik-h commented May 13, 2019

wweic left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sgrechanik-h commented May 17, 2019

tqchen commented May 17, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

derisavi commented May 21, 2019

Choose a reason for hiding this comment

derisavi left a comment

Choose a reason for hiding this comment

tqchen commented May 27, 2019

tqchen commented May 8, 2019 •

edited

Loading