8370914: C2: Reimplement Type::join

[merykitty]

Hi,

Currently, Type::join is implemented using Type::dual. The idea seems to be that the dual of a join would be the meet of the duals of the operands. This helps us avoid the need to implement a separate join operation. The comments also discuss the symmetry of the join and the meet operations, which seems to refer to the various fundamental laws of set union and intersection.

However, it requires us to find a representation of a Type class that is symmetric, which may not always be possible without outright dividing its value set into the normal set and the dual set, and effectively implementing join and meet separately (e.g. TypeInt and TypeLong).

In other cases, the existence of dual types introduces additional values into the value set of a Type class. For example, a pointer can be a nullable pointer (BotPTR), a not-null pointer (NotNull), a not-null constant (Constant), a null constant (Null), an impossible value (TopPTR), and AnyNull? This is really hard to conceptualize even when we know that AnyNull is the dual of NotNull. It also does not really work, which leads to us sprinkling above_centerline checks all over the place. Additionally, the number of combinations in a meet increases quadratically with respect to the number of instances of a Type. This makes the already hard problem of meeting 2 complicated sets a nightmare to understand.

This PR reimplements Type::join as a separate operation and removes most of the dual concept from the Type class hierachy. There are a lot of benefits of this:

• It makes the operation much more intuitive, and changes to Type classes can be made easier. Instead of thinking about type lattices and how the representation places the Type objects on the lattices, it is much easier to conceptualize a join when we think a Type as a set of possible values.
• It tightens the invariants of the classes in the hierachy. Instead of having 5 possible ptr() value when a TypeInstPtr participating in a meet/join operation, there are only 3 left (AnyNull is non-sensical and TopPTR must be an AnyPtr). This, in turns, reduces the number of combinations in a meet/join from 25 to 9, making it much easier to reason about.

This PR also tries to limit the interaction between unrelated types. For example, meeting and joining of a float and an int seem to happen only when we try to do those operations on the array types of those types. Limiting these peculiar operations to the places they happen makes it easier to catch unexpected interactions. It also helps us avoid sprinkling a bunch of cases in each meet and join method.

Future work:

• More cleanup can be made. I purposely avoid modifying the xmeet methods too much. There is a lot of room for simplification since the number of operand combinations has decreased significantly.
• Remove the remaining remnants of dual such as TypeInt::_dual and TypePtr::above_centerline.
• Stronger invariants can probably be asserted. For example, it seems that we can enforce that no instance with the concrete type being TypeOopPtr can be made, or TypePtr cannot be made with BotPTR.

Please take a look and leave your reviews, thanks a lot.

---

Progress

• Change must be properly reviewed (1 review required, with at least 1 Reviewer)
• Change must not contain extraneous whitespace
• Commit message must refer to an issue

Issue

• JDK-8370914: C2: Reimplement Type::join (Enhancement - P4)

Reviewing

Using git

Checkout this PR locally:
$ git fetch https://git.openjdk.org/jdk.git pull/28051/head:pull/28051
$ git checkout pull/28051

Update a local copy of the PR:
$ git checkout pull/28051
$ git pull https://git.openjdk.org/jdk.git pull/28051/head

Using Skara CLI tools

Checkout this PR locally:
$ git pr checkout 28051

View PR using the GUI difftool:
$ git pr show -t 28051

Using diff file

Download this PR as a diff file:
https://git.openjdk.org/jdk/pull/28051.diff

Using Webrev

Link to Webrev Comment

[bridgekeeper]

👋 Welcome back qamai! A progress list of the required criteria for merging this PR into master will be added to the body of your pull request. There are additional pull request commands available for use with this pull request.

[openjdk]

❗ This change is not yet ready to be integrated.
See the Progress checklist in the description for automated requirements.

[openjdk]

@merykitty The following label will be automatically applied to this pull request:

• hotspot-compiler

When this pull request is ready to be reviewed, an "RFR" email will be sent to the corresponding mailing list. If you would like to change these labels, use the /label pull request command.

[mlbridge]

Webrevs

• 00: Full (672d2613)

[mhaessig]

Impressive work @merykitty!

It would be good if you could explain how your new lattice definition compares to our current definition. Especially, in regard to the completeness of join, which we currently get for free from symmetry and a complete meet, and associativity and distributivity and how we have to implement the relation in Value() to keep those properties.

While I see that your definition is potentially easier to reason about, I think that you first need to convince everyone that your definition has no significant drawbacks to what we currently have simply because this change is so fundamental.

[mhaessig]

This will need a rename ;)

[merykitty]

@mhaessig Thanks for taking a look.

It would be good if you could explain how your new lattice definition compares to our current definition.

The thing is that it is easier and more intuitive to think of a Type object as a set of possible values. For example, a TypeInt represents a set of int values, and a node (e.g. an AddI) at runtime must take values that are elements of the TypeInt of that node. Thinking of a Type as a lattice point is both more unintuitive and easier to misstep.

Especially, in regard to the completeness of join, which we currently get for free from symmetry and a complete meet

It is not free, though. It requires us to prove that the type representation is symmetric and implement xmeet in a way that satisfies such symmetry. If the symmetry is not trivial, such as in the case of TypeInstPtr, it results in a meet that is harder to understand than implementing meet and join separately. It is because instead of reasoning about sets and their elements, we have to keep track of the core symmetry, and how our lattice points work with such symmetry, definitely not free. I gave up trying to have a symmetric representation when adding unsigned bounds and bit information to TypeInt and TypeLong, and just divided their lattice into the normal world and the dual world with a boolean. It may not be an actual symmetry, since I did not think about how a normal TypeInt would interact with a dual TypeInt, but it is good enough, and it is very trivial that the implementation of TypeInt::xmeet is correct.

if (_dual) {
    return do_join();
} else {
    return do_meet();
}

Another issue is that the existence of dual types doubles the set of values that can participate in a meet. For example, in TypeInstPtr, instead of implementing a meet and a join, each with 9 possible combinations, all of which are intuitive (because they represent real sets), we have to implement a meet that takes into consideration 25 input combinations.

[merykitty]

Furthermore, I believe our current representation is also not fully symmetric. For example, when meeting 2 TypeInstPtr with TopPTR, instead of intersecting their _interfaces, we union them. This is because when joining 2 TypeInstPtr with BotPTR, the duals of them would be 2 TopPTR, and since it is a join, we need to union their _interfaces. However, if we are really meeting 2 TopPTR, unioning the _interfaces would definitely be incorrect, meeting the _interfaces requires us to intersect their set of interfaces. As a result, it can be seen that the symmetry of TypeInstPtr relies on the fact that a "normal" TopPTR must have empty _interfaces.

[mhaessig]

I'm not trying to argue for symmetry. All I am trying to say is that our current type lattice has some properties, mainly associativity and distributivity, that let us apply meets and joins in arbitrary order and reach the same optimal result. Also, we need a lattice, otherwise not every pair of types have a meet or join, which would be quite cumbersome/impossible to use.

So I want to understand mathematically how you uphold these properties.

[merykitty]

For associativity and distributivity, I think we need to check for comformance of each implementation. Luckily, if for a Type object, these properties satisfy for each of its fields, then the properties satisfy for the object as a whole.

Also, we need a lattice, otherwise not every pair of types have a meet or join, which would be quite cumbersome/impossible to use.

We actually rarely need to meet/join unrelated types (e.g joining a float and an int). As a result, disallowing those operations may help us catch unwanted errors. We still have Type::TOP and Type::BOTTOM, though. Anyway, thinking of Types as lattice points is both unnecessary and makes the problems harder to comprehend.