Page MenuHomePhabricator

Support emptiness checks for unbounded FlatAffineConstraints.
ClosedPublic

Authored by arjunp on Jan 7 2021, 3:57 PM.

Details

Summary

With this, we have complete support for emptiness checks. This also paves the way for future support to check if two FlatAffineConstraints are equal.

Diff Detail

Event Timeline

arjunp created this revision.Jan 7 2021, 3:57 PM
arjunp requested review of this revision.Jan 7 2021, 3:57 PM
arjunp retitled this revision from Support emptiness checks for unbounded FlatAffineConstraints. With this, we have complete support for emptiness checks. This also paves the way for future support to check if two FlatAffineConstraints are equal. to Support emptiness checks for unbounded FlatAffineConstraints..Jan 7 2021, 3:57 PM
arjunp edited the summary of this revision. (Show Details)
arjunp updated this revision to Diff 315269.EditedJan 7 2021, 4:12 PM

Added attribution for the algorithm.

ftynse added a comment.Jan 8 2021, 1:13 AM

It looks like something went wrong when updating the second revision and the diff now only contains the comment change. Note that if you use arc diff on a branch of multiple commits, you must specify the commit that the branch is based on rather than HEAD^, which is merely the previous-to-head commit.

ftynse requested changes to this revision.Jan 8 2021, 1:13 AM
This revision now requires changes to proceed.Jan 8 2021, 1:13 AM
arjunp updated this revision to Diff 315314.Jan 8 2021, 1:34 AM

Trying to fix the patch.

arjunp added a comment.Jan 8 2021, 1:38 AM

Seems to be fixed now.

arjunp updated this revision to Diff 315321.Jan 8 2021, 2:24 AM

Resolved clang-tidy issue.

ftynse requested changes to this revision.Jan 11 2021, 9:15 AM
ftynse added inline comments.
mlir/include/mlir/Analysis/Presburger/LinearTransform.h
31 ↗(On Diff #315321)

Naming nit: a.apply(b) reads like applying b to a, but this function does the inverse. applyTo?

mlir/lib/Analysis/AffineStructures.cpp
1079

Shouldn't this be atEq?

1103

Let's not commit commented-out code

1106–1107

Or you can do

for (unsigned i = fac.getNumEqualities(); i >0; --i) 
  if (eqInvolvesSuffixDims(fac, i - 1, unboundedDims))
    fac.removeEquality(i - 1);

that is, replace uses of i with i - 1 (for long loops, just define a variable), and avoid implicit sign conversion.

1183

You may want to call removeIdRange instead. This will avoid the loop together with its signedness magic and a lot of copies that this does because of removing numBoundedDims instead of i.

mlir/lib/Analysis/Presburger/LinearTransform.cpp
14 ↗(On Diff #315321)

I suppose you wanted Matrix &&oMatrix instead. Otherwise, this makes a copy of a matrix and than moves out of that copy. If you do need a copy, consider const Matrix & instead.

16 ↗(On Diff #315321)

I don't know how to understand "remainder of division by [0, M(row, sourceCol))". Did you rather mean [0, M(row, sourceCol) be the range of values the remainder can take?

23 ↗(On Diff #315321)

Please only use auto when it improves readability, e.g. for long iterator types or where type is obvious from context such as cast.

23–24 ↗(On Diff #315321)

Note that machine integer division is rounding to zero, as opposed to Euclidean division that rounds to negative infinity. So -4 / 3 gives -1 with machine division and -2 with Euclidean division. Usually, in affine world, I'd expect the latter. If it is used further to compute the remainder, machine division will yield -4 - (-1 * 3) = -1, but one would normally expect the remainder to be non-negative -4 - (-2 * 3) = 2. Please verify that this code does what you expect it to do and, if so, add an appropriate comment (-1 = 2 mod 3 after all).

75 ↗(On Diff #315321)

Except that the code in modEntryColumnOperation doesn't do floor().

110 ↗(On Diff #315321)

Please reserve the space in the vector before pushing back in a loop.

mlir/unittests/Analysis/AffineStructuresTest.cpp
254

Please add a test that involves equalities, and a test that exercises Euclidean division when computing the row echelon form. Since these are unit tests, the latter can be easily done by testing the row echelon form computation directly.

This revision now requires changes to proceed.Jan 11 2021, 9:15 AM
arjunp updated this revision to Diff 316075.Jan 12 2021, 6:27 AM
arjunp marked 11 inline comments as done.

Address comments.

Thanks for the review!

mlir/lib/Analysis/AffineStructures.cpp
1079

Sorry, yes. Fixed and added a test case.

mlir/lib/Analysis/Presburger/LinearTransform.cpp
16 ↗(On Diff #315321)

Yes, fixed.

23–24 ↗(On Diff #315321)

Yeah, my intention was to use Euclidean division.

We can't test for this because the Euclidean GCD algorithm is still correct and terminates with machine division (about efficiency, I am not sure). It is still correct with machine division since adding _any_ multiple of one operand to the other preserves their GCD. Termination:

Suppose we run the algorithm with integers x and y. If one of x or y is divides the other then the remainder issue doesn't come into play.

Otherwise, after one iteration we have -|x| < y < |x|.

If |y| > |x|, this means |y| decreases after this iteration. Otherwise, consider the next iteration after x, y are swapped, in which the operand of greater magnitude will be set to the remainder. That operand will decrease in magnitude then. So every two iterations one of the operands decreases in magnitude as long as neither is divisible by the other.

Once one operand becomes a multiple of the other, that one gets set to zero and we are done. To test that we use Euclidean division, we would have to directly test this static free function modEntryColumnOperation.

I feel it's easier to reason about the code if both operands are made positive, so I've changed it accordingly.

mlir/unittests/Analysis/AffineStructuresTest.cpp
254

Added tests involving equalities. See above regarding the unit test for LinearTransform. The column echelon form computation works with both Euclidean and machine division.

bollu added a subscriber: bollu.Jan 12 2021, 7:20 AM
andydavis1 added inline comments.Jan 12 2021, 3:10 PM
mlir/lib/Analysis/AffineStructures.cpp
1065

Might be worth capturing this fact in local variable: unsigned dirsNumCols = getNumCols() - 1; since it is use 3 times below.

arjunp updated this revision to Diff 316329.Jan 12 2021, 11:04 PM
arjunp marked an inline comment as done.

Addressed Andy's comment.

bollu added inline comments.Jan 13 2021, 11:42 AM
mlir/lib/Analysis/AffineStructures.cpp
1066

consider

const unsigned dirsNumCols = getNumCols() - 1;

to indicate that the value isn't changed throughout the computation.

mlir/lib/Analysis/Presburger/Matrix.cpp
88

nit: eliminate unnecessary return?

mlir/lib/Analysis/Presburger/Simplex.cpp
523

Consider:

return computeOptimum(Direction::Up, con[constraintIndex]).hasValue();

instead of:

if (Optional<Fraction> opt =
        computeOptimum(Direction::Up, con[constraintIndex]))
  return true;
return false;
arjunp updated this revision to Diff 316609.Jan 14 2021, 3:21 AM
arjunp marked 3 inline comments as done.

Addressed Siddharth's commments.

We can't test for this because the Euclidean GCD algorithm is still correct and terminates with machine division (about efficiency, I am not sure).

You still can write a test computing the column echelon form for a given matrix that requires division by a negative value somewhere. The point of such a test is to (a) demonstrate that the result is correct and (b) provide enough coverage so that potential future changes in the column echelon computation affect a specific test rather than a much larger test (emptiness check) that can also be affected by dozens of other things and makes it ten times harder to find the root cause.

mlir/lib/Analysis/AffineStructures.cpp
1066

MLIR does not follow this pattern. If you prefer it had, please bring it up for general discussion rather than diverging locally.

arjunp updated this revision to Diff 316689.Jan 14 2021, 9:48 AM
arjunp marked an inline comment as done.

Added unit tests for makeTransformToColumnEchelon.

ftynse accepted this revision.Jan 14 2021, 10:23 AM

Thank you!

This revision is now accepted and ready to land.Jan 14 2021, 10:23 AM

Great! I don't have commit access, can you land this? :)

This revision was landed with ongoing or failed builds.Jan 14 2021, 10:34 AM
This revision was automatically updated to reflect the committed changes.