Be more careful when selecting LUB of free regions #27892
Conversation
probably not enough. This code is so simple, what could possibly go wrong?
important inventions of all time
closures, upper bounds, and other fun things
`TransitiveRelation`
|
cc @arielb1, this seems like something you might enjoy. |
|
Calculating the LUB of |
|
@arielb1 I could probably throw it in, but OTOH you can do quite a bit better in that case since it's a tree. If we did a bit of pre-calculation, we could do LUB support very fast. |
|
@arielb1 iirc the current code is super naive, using hashmaps and the like. premature optimization and all that. |
|
@arielb1: it's taking me a while to find time to review this, so if you want to r? the PR please feel free! (Just let me know.) |
|
I want somebody to look at the algorithm. |
|
r? @pnkfelix |
| @@ -10,24 +10,18 @@ | |||
|
|
|||
| //! This file defines | |||
| /// Returns the set of bounds `X` such that: | ||
| /// | ||
| /// - `a < X` and `b < X` | ||
| /// - there is no `Y` such that `a < Y` and `Y < X` |
There was a problem hiding this comment.
This definition for the returned set of bounds does not seem adequate.
-
A reader might rightfully wonder "does the range of Y in the second condition include the elements of X? Or is X excluded from the universe of Y?"
(From reading the code overall I concluded that the universe of Y does indeed include the elements of X, which leads us to the second issue...)
-
It does not cover what happens for situations with strongly-connected-components such as:
c -> d d -> c a -> c b -> dI infer, from the tests that come later in the PR, that in a case like the above,
minimal_upper_bounds(a, b)will return either[c]or[d]; but neither of those options conforms with the specification.
Update: I just re-read the definition more carefully and realized that it only says "there is no Y such that a < Y and Y < X -- namely, it does not mention b anywhere, though I inferred (perhaps incorrectly) that the "a < Y" condition was meant to cover b as well, as in lets say "there is no Y such that a < Y and b < Y and Y < X."
- This means that, as stated,
minimal_upper_boundsin my above example with an SCC in fact can return[c]without violating any of the conditions it listed.
So I'm rethinking my criticism, it could be that this was very carefully crafted to allow for a consistent choice in the case of reaching an SCC. But if that is the case, this comment would greatly benefit from mentioning the SCC case and pointing out the intent here.
Update 2: I don't think my attempt to make sense of the original definition works out. It may well be that a is indeed meant to have some special role, but if you consider something like
a -> c
c -> d
b -> d
then that should obviously yield [d], but by the definition above, choosing Y == c would cause the second condition to be violated. That is, I think the second condition does need to be revised to include b in some role, to cover the behavior in such situations.
There was a problem hiding this comment.
Thanks for trying to shared to make sense of it, I think I was just imprecise in writings things out (though I certainly considered the SCC case). (The answer for SCCs is that we pick the lowest numbered element of the SCC as its representative.)
There was a problem hiding this comment.
Here is a set of tests I sketched while thinking about cases of interest here. (However, given that you've pointed out that the SCC answer is that we pick the lowest numbered element, and not that a has some special role, then a number of these tests will be arguably redundant.)
http://blog.pnkfx.org/linked/lub-graphs.html
(View source to see graphviz text for each case. Or actually I'll just add that to the rendering.)
| // not minimal upper bounds. So you may have e.g. | ||
| // `[a, b, tcx, x]` where `a < tcx` and `b < tcx` and | ||
| // `x < a` and `x < b`. This could be reduced to | ||
| // just `[x]`. |
There was a problem hiding this comment.
When I first read this comment I was confused as to what step, if any, the "This could be reduced to just [x]" was referring to. After reading the whole thing, I understood that it was saying that [x] is the expected output from the whole series of steps. I think the presentation would be improved if you gave the concrete hypothetical input [a, b, tcx, x] at the outset, before the first step.
|
So I had a bunch of nits, but of course the real question is about the algorithm being used. It seems reasonable at first glance. If the element order were preserved as elements were removed from the vector then I would be more confident in its correctness. But the use of |
So as I wrote, I'm pretty sure it's fine, because the algorithm is working its way left-to-right, and you can reorder the "not yet processed" things as you like. But it is somewhat subtle. I could rewrite it to compress-and-truncate, but then I'd either want a copy bound or a lot of calls to clone. Either of which is fine really, but...perhaps I'll just leave a comment. |
|
oh, wait, I forgot, my vector is just indices. Yeah, ok, I'll remove the subtle call to swap_remove. |
|
@pnkfelix how about "postdom_upper_bound"? |
|
/me decides on his own. |
|
@bors r=pnkfelix |
|
📌 Commit 81eab1c has been approved by |
Issue #27583 was caused by the fact that `LUB('a,'b)` yielded `'static`, even if there existed a region `'tcx:'a+'b`. This PR replaces the old very hacky code for computing how free regions relate to one another with something rather more robust. This solves the issue for #27583, though I think that similar bizarro bugs can no doubt arise in other ways -- the root of the problem is that the region-inference code was written in an era when a LUB always existed, but that hasn't held for some time. To *truly* solve this problem, it needs to be generalized to cope with that reality. But let's leave that battle for another day. r? @aturon
|
⌛ Testing commit 81eab1c with merge 5e5b99f... |
Issue #27583 was caused by the fact that
LUB('a,'b)yielded'static, even if there existed a region'tcx:'a+'b. This PR replaces the old very hacky code for computing how free regions relate to one another with something rather more robust. This solves the issue for #27583, though I think that similar bizarro bugs can no doubt arise in other ways -- the root of the problem is that the region-inference code was written in an era when a LUB always existed, but that hasn't held for some time. To truly solve this problem, it needs to be generalized to cope with that reality. But let's leave that battle for another day.r? @aturon