[mlir][presburger] Preserve relative ordering of symbols and non-symbol vars when setting up SymbolicLexSimplex #119036
Conversation
christopherbate
changed the title
…ol vars when setting up SymbolicLexSimplex The Presburger library's SymbolicLexSimplex class organizes its tableau so that symbols occuply the columns in the range `[3, 3 + num_symbols)`. When creating the SymbolicLexOpt from an IntegerRelation, the API allows the user to specify what variables of the system should be considered as symbols. The constructor then reorders the coefficient when constructing the initial constraint rows. This reordering was also manually at certain users of SymbolicLexOpt, e.g. `IntegerRelation::computeReprWithOnlyDivLocals`. Previously, at least one of the reordering implementations was not stable (in `computeReprWithOnlyDivLocals`). If it considered the the second variable to be a symbol in a 4 variable system: ``` var0 sym1 var2 var3 ``` then the simplex would get arranged as ``` sym1 var3 var2 var0 ``` I discovered tha, in certain cases, this reordering can cause `SymbolicLexOpt::computeSymbolicLexMax` to become extremely inefficient due to a large number of branches through the context tableau as well as an explosion in the size of the coefficients. See the additional test added. So, this change updates the locations where the reordering logic is implemented in order to ensure the partitioning is stable. It is possible that this is just masking a more complicated bug (hard to say for a non-expert on this code). My debugging efforts lead me to believe that there is not a bug in the simplex solver, however. Rather, some pre-processing procedures that rely on heuristics/patterns (e.g. detection of division representations) can fail, which can result in a sub-optimal problem description being handed off to the simplex solver. In any case, a non-stable partitioning of the variables is unexpected and makes it difficult to proactively try to avoid problematic system descriptions by users of the Presburger library.
christopherbate
force-pushed
the
mlir-presburger-compute-repr-fix
branch
from
91d1aa9 to
3702927
Compare
|
@llvm/pr-subscribers-mlir-presburger @llvm/pr-subscribers-mlir Author: Christopher Bate (christopherbate) ChangesThe Presburger library's SymbolicLexSimplex class organizes its tableau When creating the SymbolicLexOpt from an IntegerRelation, the API allows Previously, at least one of the reordering implementations was not stable then the simplex would get arranged as I discovered tha, in certain cases, this reordering can cause So, this change updates the locations where the reordering logic It is possible that this is just masking a more complicated bug (hard to Full diff: https://github.com/llvm/llvm-project/pull/119036.diff 3 Files Affected:
diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index 74cdf567c0e569..15d453896924af 100644
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
@@ -229,25 +229,17 @@ PresburgerRelation IntegerRelation::computeReprWithOnlyDivLocals() const {
// SymbolicLexOpt requires these to form a contiguous range.
//
// Take a copy so we can perform mutations.
- IntegerRelation copy = *this;
std::vector<MaybeLocalRepr> reprs(getNumLocalVars());
- copy.getLocalReprs(&reprs);
+ this->getLocalReprs(&reprs);
- // Iterate through all the locals. The last `numNonDivLocals` are the locals
- // that have been scanned already and do not have division representations.
unsigned numNonDivLocals = 0;
- unsigned offset = copy.getVarKindOffset(VarKind::Local);
- for (unsigned i = 0, e = copy.getNumLocalVars(); i < e - numNonDivLocals;) {
- if (!reprs[i]) {
- // Whenever we come across a local that does not have a division
- // representation, we swap it to the `numNonDivLocals`-th last position
- // and increment `numNonDivLocal`s. `reprs` also needs to be swapped.
- copy.swapVar(offset + i, offset + e - numNonDivLocals - 1);
- std::swap(reprs[i], reprs[e - numNonDivLocals - 1]);
- ++numNonDivLocals;
+ llvm::SmallBitVector isSymbol(getNumVars(), true);
+ unsigned offset = getVarKindOffset(VarKind::Local);
+ for (unsigned i = 0, e = getNumLocalVars(); i < e; ++i) {
+ if (reprs[i])
continue;
- }
- ++i;
+ isSymbol[offset + i] = false;
+ ++numNonDivLocals;
}
// If there are no non-div locals, we're done.
@@ -266,9 +258,10 @@ PresburgerRelation IntegerRelation::computeReprWithOnlyDivLocals() const {
// and the returned set of assignments to the "symbols" that makes the lexmin
// unbounded.
SymbolicLexOpt lexminResult =
- SymbolicLexSimplex(copy, /*symbolOffset*/ 0,
+ SymbolicLexSimplex(*this,
IntegerPolyhedron(PresburgerSpace::getSetSpace(
- /*numDims=*/copy.getNumVars() - numNonDivLocals)))
+ /*numDims=*/getNumVars() - numNonDivLocals)),
+ isSymbol)
.computeSymbolicIntegerLexMin();
PresburgerRelation result =
lexminResult.lexopt.getDomain().unionSet(lexminResult.unboundedDomain);
diff --git a/mlir/lib/Analysis/Presburger/Simplex.cpp b/mlir/lib/Analysis/Presburger/Simplex.cpp
index 4ffa2d546af4dd..384dc05cbcbc01 100644
--- a/mlir/lib/Analysis/Presburger/Simplex.cpp
+++ b/mlir/lib/Analysis/Presburger/Simplex.cpp
@@ -64,13 +64,14 @@ SimplexBase::SimplexBase(unsigned nVar, bool mustUseBigM,
const llvm::SmallBitVector &isSymbol)
: SimplexBase(nVar, mustUseBigM) {
assert(isSymbol.size() == nVar && "invalid bitmask!");
- // Invariant: nSymbol is the number of symbols that have been marked
- // already and these occupy the columns
- // [getNumFixedCols(), getNumFixedCols() + nSymbol).
- for (unsigned symbolIdx : isSymbol.set_bits()) {
- var[symbolIdx].isSymbol = true;
- swapColumns(var[symbolIdx].pos, getNumFixedCols() + nSymbol);
- ++nSymbol;
+ // Iterate through all the variables. Move symbols to the left and non-symbols
+ // to the right while preserving relative ordering.
+ for (unsigned i = 0; i < nVar; ++i) {
+ if (isSymbol[i]) {
+ var[i].isSymbol = true;
+ swapColumns(var[i].pos, getNumFixedCols() + nSymbol);
+ nSymbol++;
+ }
}
}
diff --git a/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp b/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
index 8e31a8bb2030b6..7561d2044bd775 100644
--- a/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
@@ -855,6 +855,20 @@ TEST(SetTest, computeReprWithOnlyDivLocals) {
PresburgerSet(parseIntegerPolyhedron(
{"(x) : (x - 3*(x floordiv 3) == 0)"})),
/*numToProject=*/2);
+
+ testComputeRepr(
+ parseIntegerPolyhedron("(e, a, b, c)[] : ("
+ "a >= 0,"
+ "b >= 0,"
+ "c >= 0,"
+ "e >= 0,"
+ "15 - a >= 0,"
+ "7 - b >= 0,"
+ "5 - c >= 0,"
+ "e - a * 192 - c * 32 - b * 4 >= 0,"
+ "3 - e + a * 192 + c * 32 + b * 4 >= 0)"),
+ parsePresburgerSet({"(i) : (i >= 0, i <= 3071)"}),
+ /*numToProject=*/3);
}
TEST(SetTest, subtractOutputSizeRegression) {
|
Superty
left a comment
Superty
left a comment
There was a problem hiding this comment.
Hi, thanks for the patch! This looks great. I left some comments. Once these are addressed, we should be good to go.
It does seem concerning if the Simplex becomes slow after reordering some variables. Do I understand correctly that you can reproduce the slowness by using the modified variable ordering in the initial test case? If not, I don't understand why it should be slow if the reordering occurs internally but not externally. Either way, as you say, your patch makes sense regardless. I will look into the Simplex issue further later. Thanks for reporting it!
(Sorry about the delay, I was on vacation. As a heads up, I may not have great availability for the coming week either, but hopefully all I'll need to do is approve it! :))
| for (unsigned i = 0; i < nVar; ++i) { | ||
| if (isSymbol[i]) { | ||
| var[i].isSymbol = true; | ||
| swapColumns(var[i].pos, getNumFixedCols() + nSymbol); | ||
| nSymbol++; | ||
| } |
There was a problem hiding this comment.
The new code looks equivalent to the old -- am I missing someting?
There was a problem hiding this comment.
I suppose set bits doesn't guarantee the order of indices returned?
There was a problem hiding this comment.
You're right, it was equivalent. I updated the code to use a stable partitioning.
There was a problem hiding this comment.
(The old code in computeReprWithOnlyDivLocals was not preserving the relative order of symbols while this SimplexBase constructor was not preserving the relative order of non-symbols. The updated code ensures the partitioning is now stable.)
Yes, the test I added will demonstrate the slowness without the additional changes added here. |
|
Hey, I think I wasn't very clear. What I meant is that we can extract the calls to the Simplex made in the old code and make a test case out of that. That test case will still be slow even after this patch. Is that correct? Thanks! |
|
(I am not insisting you look into that for this patch; I'm just checking my understanding of the situation!) |
|
Sorry for the delayed update/response. Planning to address your comments tonight then will push an update.
Oh, yes, I think I can create a test-case that shows the slowness even after the patch (it just has to do with the ordering of the variables, we can use the test case I added in the patch and just change the order). However, when I was in the middle of debugging this two weeks ago, I convinced myself that the slowness was correct (but now I'm not so sure). I'd like to know the algorithm well enough to verify using pen-and-paper, but I'm still studying it. You have an iteration space of shape When phrased this way, if you treat Let's say you reorder the variables to Now Regardless of the order of how variables The algorithm would then have added the constraint |
|
Hi, Thanks for your reply. I understand that the ordering Arjun |
|
By the way, here's a simpler reproducer |
…g columns. When the SimplexBase constructor reorders columns into symbol and non-symbol segments, use a stable partitioning.
|
@Superty I addressed all your comments and am passing existing tests. However, while testing in my downstream project, I'm seeing failures where I'm now hitting this unreachable (https://github.com/llvm/llvm-project/blob/main/mlir/lib/Analysis/Presburger/Simplex.cpp#L1463) in uses of Simplex unrelated to what motivated this bug originally. This makes me think that perhaps this change, while still good cleanup of I'll need to investigate more tomorrow. |
|
@christopherbate I have a few fixes so far from looking into your earlier test case, can you try rebasing on https://github.com/Superty/llvm-project/tree/debug-pip and see if it still fails? If so, I'm happy to look into this as well if you send a test case. |
|
I tested with your changes as well and unfortunately it doesn't resolve the issue. I'm working on finding an isolated reproducer now. I also find that preferring non-symbolic cuts seems to slow down the test added in this change. |
|
The |
Superty
left a comment
Superty
left a comment
There was a problem hiding this comment.
Hi, sorry about the delay. I mistakenly thought that this was blocked on opening the other issue. This looks good to me overall, but please address the two comments I just left before landing. Thanks for the PR! Looking forward to investigating a reproducer for the other issue.
| // segment of non-symbol up until the current variable's column are | ||
| // shifted to the right and the current column is then moved before the | ||
| // right-shifted segment. | ||
| tableau.moveColumns(var[i].pos, 1, getNumFixedCols() + nSymbol); |
There was a problem hiding this comment.
since the tableau has zero rows at this point, there is no need to move columns in it.
There was a problem hiding this comment.
Probably a good idea to leave a comment to that effect.
| for (unsigned col = getNumFixedCols() + nSymbol; col < var[i].pos; ++col) | ||
| unknownFromColumn(col).pos = col + 1; | ||
|
|
||
| // Perform the equivalent rearrangement on the col-to-unknown | ||
| // mapping. | ||
| std::rotate(colUnknown.begin() + getNumFixedCols() + nSymbol, | ||
| colUnknown.begin() + var[i].pos, | ||
| colUnknown.begin() + var[i].pos + 1); | ||
|
|
||
| // Update the column mapping for the current variable. | ||
| var[i].pos = getNumFixedCols() + nSymbol; | ||
| var[i].isSymbol = true; | ||
|
|
||
| ++nSymbol; | ||
| } |
There was a problem hiding this comment.
I find this hard to reason about :(
I would prefer an approach like this:
// First we assign the correct column positions in the `var` vector,
// then we update the `colUnknown` vector to be consistent with this.
int curColumn = getNumFixedCols();
for (unsigned i = 0; i < nVar; ++i) {
if (isSymbol[i]) {
nSymbol++;
var[i].isSymbol = true;
var[i].pos = curColumn;
curColumn++;
}
}
for (unsigned i = 0; i < nVar; ++i) {
if (!isSymbol[i]) {
var[i].pos = curColumn;
curColumn++;
}
}
for (unsigned i = 0; i < nVar; ++i)
colUnknown[var[i].pos] = i;There was a problem hiding this comment.
I didn't fully check that the two are equivalent but you get the idea.
3 participants
The Presburger library's SymbolicLexSimplex class organizes its tableau
so that symbols occuply the columns in the range
[3, 3 + num_symbols).When creating the SymbolicLexOpt from an IntegerRelation, the API allows
the user to specify what variables of the system should be considered
as symbols. The constructor then reorders the coefficient when constructing
the initial constraint rows. This reordering was also manually at certain
users of SymbolicLexOpt, e.g.
IntegerRelation::computeReprWithOnlyDivLocals.Previously, at least one of the reordering implementations was not stable
(in
computeReprWithOnlyDivLocals). If it considered the the secondvariable to be a symbol in a 4 variable system:
then the simplex would get arranged as
I discovered tha, in certain cases, this reordering can cause
SymbolicLexOpt::computeSymbolicLexMaxto become extremely inefficientdue to a large number of branches through the
context tableau as well as an explosion in the size of the coefficients.
See the additional test added.
So, this change updates the locations where the reordering logic
is implemented in order to ensure the partitioning is stable.
It is possible that this is just masking a more complicated bug (hard to
say for a non-expert on this code). My debugging efforts lead me to believe
that there is not a bug in the simplex solver, however.
Rather, some pre-processing procedures that rely on
heuristics/patterns (e.g. detection of division representations) can fail,
which can result in a sub-optimal problem description
being handed off to the simplex solver. In any case, a non-stable
partitioning of the variables is unexpected and makes it difficult to
proactively try to avoid problematic system descriptions by users of the
Presburger library.