Can the rt2 <: rt1 constraint on br_on_cast* instructions be relaxed?

[tlively]

Implementing the latest versions of the br_on_cast instructions in Binaryen, I realized that the rt2 <: rt1 constraint is slightly painful for us to accommodate. Binaryen discards the input type annotation after parsing and reconstructs it from the type of the operand when printing or emitting a module. Before the module is emitted, the optimizer may have been able to refine the type of the operand, which would result in a more refined input type annotation being emitted. However, the operand type may have been refined such that it is no longer a supertype of the cast target type. Obviously this means the cast must fail and can be optimized out, but it would be unfortunate if Binaryen were forced to do that optimization just to emit a valid module.

We could work around this by treating the input type of a br_on_cast instruction as the LUB of the actual input type and the cast target type, but that would lose precision in the output type, which could adversely affect other optimizations.

It would be easier, more efficient, and better for optimizations to simply drop the requirement that rt2 <: rt1 instead. AFAICT, the only downside of doing this is that we would need to replace it with a weaker constraint that rt1 and rt2 are in the same hierarchy (i.e. have a common supertype), which is slightly more complex to express.

@rossberg, WDYT?

[Liedtke]

To provide a second data point: For the V8 implementation the subtype restriction was easy to implement (it's still an additional check) but for our fuzzer which has to generate correct type immediates, it was surprisingly painful.

[rossberg]

It's possible. The main technical downside is that it is likely to complicate the computation of type differences in the future, e.g., if we are to add union types in some form or other refinements to the type hierarchy. Then that would turn into a lub/glb-like operation in the engine, which worries me slightly.

(An additional, social downside might be that it can cause more confusion about the role of casts -- some people already seemed to believe that they need to insert upcasts, too, which would then in fact be legal but pointless. But I don't think we ought to worry about that.)

[tlively]

Can you say more about how this might complicate things in the future? An example would help.

I agree we shouldn't worry too much about folks getting confused about when casts are necessary. Binaryen will optimize out obviously unnecessary casts and I expect folks will figure it out pretty fast when experimenting with code gen.

[tlively]

ping @rossberg. For now, I'll put this on the agenda for tomorrow's subgroup meeting.

[rossberg]

Imagine we have a union type A = C ∪ D and cast it to some B, so that we need to find A-B. With the subtype constraint, we know that B must be a subtype of either C or D (or both). To compute the difference, I expect we can just check subtyping for each individually and either keep that part of the union or remove it. Without the constraint, there may be cases where B only has a common subtype with e.g. C. We'd still need to remove it then. But checking whether there is a common subtype is no easier than computing that common subtype via the glb.

Another point that occurred to me and is more immediately relevant is that relaxing this constraint is making type information less precise, in ways that could be practically relevant. Types that are closer together generally require shorter code sequences than others (a consequence of our monolithic cast instruction). I assume that an engine wants to produce the shortest possible code. To do that, it will first need to find the smallest type from which to cast down -- in the absence of a subtype constraint, that is effectively the lub between source and target type. That is, the engine now has to compute the same lub that we just saved the consumer from computing. So in practice, this looks like it's shifting work from producer to consumer, which is the wrong direction. Plus, it introduces a form of lub computation through the backdoor.

[conrad-watt]

Just fyi I may not be able to make the meeting tomorrow, but I'd also be a little concerned about this change. The subtype constraint is the naively "correct" one, and relaxing it to something less regular as a snap judgement might come back to bite us later.

Could binaryen preserve the input type annotation in the IR? Presumably any refinements to the actual input type wouldn't affect the well-typedness of the instruction - the input annotation could be optionally refined, but if the aim is "minimum engineering time to emit valid code", emitting the original annotation would be sufficient.

EDIT: unless this would have implications for refinement of the type along the "cast fail" path...

[tlively]

Sorry @rossberg, I still don't understand your examples.

Without the constraint, there may be cases where B only has a common subtype with e.g. C. We'd still need to remove it then.

Here's the case analysis as far as I can figure it out for the unconstrained case in the presence of union heap types:

1. B is a strict subtype of C or D and unrelated to the other. Without loss of generality, assume B <: C. In this case, failure to cast to B does not rule out either C or D, so the type of the failure arm is A (i.e. C ∪ D).

2. B is a supertype of C or D or both. Without loss of generality, assume B :> C. If the value is a C, the cast definitely succeeds, so we can remove C from the type of the failure arm, leaving only D. Each type in the union can be independently considered for exclusion in the same way. In fact, if we relax the subtyping constraint in the MVP, we could already express this in the definition of type difference and have the failure arm return bottom when casting to a supertype.

3. B is otherwise related to both C and D. If B is a subtype of one and a supertype of the other, then without loss of generality, assume C <: B <: D. Then C ∪ D = D, so I assume this union type would be either invalid or an alias for D, in which case this degenerates to the MVP case. Otherwise, B must be a subtype of both C and D, in which case this similarly degenerates to the MVP case, assuming we don't allow multiple supertype definitions because that would break principal typing.

4. B is unrelated to both C and D. The cast cannot succeed, so the success arm can be typed with bottom and the failure arm can be typed with A (i.e. C ∪ D).

Taken altogether, a more powerful definition of type difference for the MVP would be:

(ref null ht1) \ (ref null ht2) = (ref ht1 \ ht2)
(ref null1? ht1) \ (ref ht2) = (ref null1? ht1 \ ht2)
ht1 \ ht2 = ⊥, if ht1 <: bt2
ht1 \ ht2 = ht1, otherwise

Note that this definition is more precise than the current definition for ht1 = ht2, so it is an improvement even if we continue requiring ht1 :> ht2. Also note that refining the success arm to ⊥ when ht1 and ht2 are unrelated requires a larger refactoring of typing rule because the success arm does not use type difference. Assuming the subtype check is constant time, this more powerful MVP type difference would be constant time.

Extended in the presence of union heap types, heap type difference would be:

(ht1_1 ∪ ... ∪ ht1_n) \ (ht2_1 ∪ ... ∪ ht2_m) = (ht1_1 \ ht2_1) ∪ ... ∪ (ht1_1 \ ht2_m) ∪ ... ∪ (ht1_n \ ht2_1) ∪ ... ∪ (ht1_n \ ht2_m)

This would have time O(nm), which seems as good as you could hope for with union types.

But checking whether there is a common subtype is no easier than computing that common subtype via the glb

But glb(A, B) can be computed in constant time, since it is either A if A <: B or B if B <: A or ⊥ otherwise. Again, this is assuming we don't have multiple supertypes because that breaks principal typing.

Types that are closer together generally require shorter code sequences than others (a consequence of our monolithic cast instruction)

Under our common assumptions about constant time cast implementations so far, I don't see how this is true.

@conrad-watt,

Your edit is correct that maintaining the unrefined input type would make the output type less precise. The goal is not just to save engineering effort, but to save engineering effort while still using the most precise type information possible for optimizations.

[rossberg]

Yeah, sorry, I screwed up the example. However, note that under the current subtype constraint, the only possible version of your cases (2) and (3) is that B = C, which is a simpler condition. So right now, the difference function would only need to search for equal types in a union, not perform any subtyping check.

Note that this definition is more precise than the current definition for ht1 = ht2, so it is an improvement even if we continue requiring ht1 :> ht2.

Ah, interesting observation. I guess we could implement this refinement. Though it’s probably not worth it, because this case only arises from pointless casts.

But glb(A, B) can be computed in constant time, since it is either A if A <: B or B if B <: A or ⊥ otherwise. Again, this is assuming we don't have multiple supertypes because that breaks principal typing.

I think you are extrapolating too much from the current state of affairs. For example, generics change the picture, because subtype checks become linear in the number of their parameters. And we may have multiple super types in the future, if they can be restricted in some ways to avoid these problems.

I don’t want to make predictions, but it is dangerous to assume that everything remains as simple as it is now.

Under our common assumptions about constant time cast implementations so far, I don't see how this is true.

Even constant time does not imply equal cost. For example:

• Casting (ref any) to (ref $t) is cheaper than casting (ref null any) to (ref $t), because we don’t have to test for null.

• Casting (ref struct) to (ref $t) is cheaper than casting (ref any) to (ref $t), because we don’t have to test for the shape of the object.

where “cheaper” means both less code and fewer instructions executed.

This is just for what we have now. With more features there will likely be more differences, and some cases may not even be constant time anymore, see above. I assume engines still want to find the shortest code sequence in each case.

[tlively]

With regards to the backdoor LUB calculation you were concerned about, calculating a precise LUB is unnecessary. It suffices to find the least abstract upper bound, which is much simpler. This is because increasing the precision of a concrete upper bound does not make the cast any simpler. (Again, under current assumptions about how casts are implemented)

In any future extension, the only possible relations between the input and output type are strict subtype, strict supertype, equal, or unrelated. It seems implausible to suggest that evaluating this relation will be prohibitively expensive, given how frequently validation needs to check subtyping already, especially when the evaluation can be boiled down to checking just ht1 <: ht2 and ht2 <: ht1

[conrad-watt]

Your edit is correct that maintaining the unrefined input type would make the output type less precise. The goal is not just to save engineering effort, but to save engineering effort while still using the most precise type information possible for optimizations.

Could Binaryen track the original input type annotation, but only emit it if the refined input type falls outside rt2 <: rt1?

i.e. use the refined input type wherever possible, otherwise default back to the original annotation?

EDIT: if the type refinement happens in stages, causing the "cast fail" path to be repeatedly refined, the "tracked" input type annotation could also be updated to record the last safe refinement.

[rossberg]

If an engine has to code-gen for (ref.cast t1 t2), then it knows that the input has type t1. So the actual code sequence it wants to generate a check for is whatever aspect of t2 is not subsumed by t1. In general, that is exactly what (ref.cast lub(t1,t2) t2) would check for, so the jit will implicitly need to compute that or some approximation. In the current system, a cheaper approximation that is restricted to an abstract type may suffice, but that is unlikely to hold up under interesting extensions like generics or unions, so it would seem unwise to build it in as a design assumption.

We have gone to lengths to avoid lubs/glbs in the past, because of the potential cost. This change does not seem important enough to turn around on that strategy. Especially since it's just work that the producer could already do offline. If that work is easy, then it should be easy for the producer as well. If not, even more reason the producer does it.

[tlively]

At least the LUB calculation would be an optional optimization. Baseline compilers certainly wouldn't be forced to implement it if the cost isn't justified, and optimizing tiers already do much more complex calculations.

To comply with the subtype constraint when emitting modules, binaryen would have to:

1. Take the LUB of the refined input type and the output type and make that the new input type
2. Either:
   • Insert another cast down to the original, refined input type on the failure arm
   • or drop the result on the failure arm and use a scratch local and possible additional non-null cast to propagate the original value instead

Without the second step, we might emit an invalid module because we might have optimized the failure arm to expect the more refined type.

Is maintaining the subtype constraint really worth forcing us to insert extra casts? I would hope not.

[conrad-watt]

@tlively does the above suggestion I sketched, where Binaryen associates an input annotation to each cast (possibly progressively updated), not work?

In your sketch above, Binaryen has already propagated the refined input type through the whole failure arm, requiring post-hoc insertion of downcasts, but surely there's some mechanism to prevent this propagation in the first place if it's the result of an ill-typed (in the current setting) input to the downcast operation - either by tracking the last "good" refinement as I suggested above, or through some other approach.

I don't think that our first solution for this kind of implementation speed bump in Binaryen should be a core spec change (that has to be propagated through other engines, tests etc), especially one that potentially has long-term ramifications for our object type system. We can always relax our type system later, but we can't un-relax it.

[rossberg]

To be honest, I am a bit puzzled that, assuming the input is well-typed, optimising it can lead to either ill-typed casts or requires the introduction of additional casts. If that's the case, then there seems to be a deeper issue with some of the transformations Binaryen is applying. Wouldn't it imply that these optimisations aren't type-preserving, i.e., unsound in general? Can you give an example of how that could happen?

When targeting a typed language it is a common hazard to throw away too much type information (e.g., the OCaml Wasm backend is dealing with similar problems). It sounds like Binaryen is trying to avoid keeping around the second type annotation we now have, perhaps that's part of the issue?