This is an archive of the discontinued LLVM Phabricator instance.

[MLIR][FlatAffineConstraints] Add support for extracting divisions with tighter bounds
ClosedPublic

Authored by Groverkss on Dec 4 2021, 5:15 AM.

Details

Summary

This patch adds support for extracting divisions when the set contains bounds
which are tighter than the division bounds. For example:

 3q - i + 2 >= 0                       <-- Lower bound for 'q'
-3q + i - 1 >= 0                       <-- Tighter upper bound for 'q'

Here, the actual upper bound for division for q would be -3q + i >= 0, but
since this actual upper bound is implied by a tighter upper bound, which awe can still
extract the divison.

Diff Detail

Event Timeline

Groverkss created this revision.Dec 4 2021, 5:15 AM
Groverkss requested review of this revision.Dec 4 2021, 5:15 AM
arjunp requested changes to this revision.Dec 6 2021, 5:29 AM

Thanks for the patch!

What we are really supporting is tighter bounds that imply the standard division bounds right? I would change the title to reflect that. Also, the first line of the summary is not clear to me.

While extracting divisions from local variables, due to additional constraints,
the original upper bound of the floor division may be removed.

Is it really removed while extracting divisions or before?

mlir/lib/Analysis/AffineStructures.cpp
1241–1255

I feel that this doesn't explain why it is valid to check this condition, i.e., why does this imply that we have a division? I would start by saying that we also support detecting divs from bounds that are strictly tighter than the division bounds described above still define a division representation, since the tighter bounds imply the division bounds.

Then finally I would give the example and mention that this can occur for example, because of the tighter bounds making the division bounds redundant, thus causing them to be removed.

1254–1256

"relaxed lower bound" seems misleading, because the lower bound here is either original one or actually tighter. (Even though the condition is relaxed in that we allow both the original bound and tighter bounds.)

1254–1256

This section was pretty confusing at first for me personally. I didn't immediately realize that you meant that Sum of constants >= 0 is equivalent to divisior - 1 - c >= 0, and so on. Writing iff on the left of the second and third lines for each constraint would help.

1255

Also, another thing I was wondering when I first saw this is, why can't we also support a tighter upper bound, i.e., c <= expr - divisior * id <= d.
Of course the answer is that WLOG you can set d = divisior - 1 by adding divisior - 1 - d to all three sides of the equation, increasing c and the constant term of expr. I would probably write something to this effect in the documentation:

WLOG we consider the upper bound to be `divisor - 1`, by defining that if the constant term of the upper bound inequality is `p`, then `divisor - 1 - p` is the constant term in `expr` and hence that inequality gives an upper bound of `divisor - 1` on `expr - divisor * id`.

Also, if you explain it this way, you can also directly obtain the constant term of expr at the start as divisor - 1 - p and then obtain c by subtracting the constant term of expression from the lower bound. Then you can check the bounds on c directly, which might be cleaner than explaining why we are checking bounds on the sum of constants below. Anyway I leave it to you to decide which is easier to understand.

1257
1257

Please set divisor before this and compare with divisor - 1. Then it will be immediately clear what we are doing here.

IMO if (!(constantSum <= divisor - 1)) is much more readable

1257

IMO if(!(constantSum >= 0)) is better

1291

Maybe not for this patch, but you can std::move here.

mlir/unittests/Analysis/AffineStructuresTest.cpp
693–745

Please add a test case like 0 <= x - 3q <= 3, where no division representation should be found.

698–699

Can you explain the test case a bit more? Where is the inequality that makes it redundant?

This revision now requires changes to proceed.Dec 6 2021, 5:29 AM
Groverkss updated this revision to Diff 393487.Dec 10 2021, 7:45 AM
Groverkss marked 8 inline comments as done.
  • Simplify implementation
  • Update unit tests
mlir/lib/Analysis/AffineStructures.cpp
1255

I don't find this easier to understand :( I tried to simplify the doc as best as I could.

Groverkss retitled this revision from [MLIR][FlatAffineConstraints] Add support for extracting divisions with redundant upper bound to [MLIR][FlatAffineConstraints] Add support for extracting divisions with tighter bounds.Dec 10 2021, 8:40 AM
Groverkss edited the summary of this revision. (Show Details)
arjunp accepted this revision.Dec 10 2021, 2:54 PM

LGTM, minor documentation comments below.

mlir/lib/Analysis/AffineStructures.cpp
1228–1229

We may as well use the same div as above (with tighter constraints) and say that these constraints also imply the same div. That makes it easier to read

1257–1258
1267–1283
1268
1269
1274
1279
1287–1291
mlir/unittests/Analysis/AffineStructuresTest.cpp
696
719
725
This revision is now accepted and ready to land.Dec 10 2021, 2:54 PM
Groverkss marked 11 inline comments as done.
  • Address Arjun's comments