Type annotations on new instructions

[rossberg]

So far, Wasm has been consciously designed such that the type of every instruction is self-contained. That is, every operand's type is either fully known (possibly with the help of a type immediate) or fully polymorphic.

With instructions like call_ref or func.bind this design choice starts to become a nuisance, and will be even more so under future extensions like those of the GC proposal. Redundant type annotations can also increase the cost of validation, since more types needs to be compared against each other (although it's not clear whether this extra cost is relevant, given the relative infrequency of most affected instructions).

Currently, the proposal omits the type on call_ref and the source type on func.bind. It requires constype immediates on null-related instructions, though, to be consistent with the instructions in the reference types proposal. Should more annotations be added for consistency and ease of type checking, or more removed for convenience/compactness?

[RossTate]

More examples of instructions that could or could not have redundant type annotations:

• input type annotation of block
• input type annotation of if
• output type annotation of loop
• input type annotation of try
• input and output type annotations of let

There will likely me many more such instructions in future proposals. For example, input and output type annotations for many of the instructions for stack primitives are redundant.

[rossberg]

@RossTate, yeah, but as mentioned elsewhere, block typing has sailed long ago, and changing it now would be rather tough. In any case, it's outside the scope of this proposal.

[RossTate]

That discussion indicated that the rationale behind the decision was that eliminating type annotations would complicate the pseudo-code interpreter by requiring end to check if the construct had an associated out-annotation and, if so, to restrict the outgoing types to that annotation and check them for compatibility.

That decision was also made at a time where only one block-like structure did not need an out-annotation, making the complexity seem unnecessary. But let will be another example where such an out-annotation is unnecessary, and there will likely be more examples down the line. let also introduces new complexities to end, such as cleaning up the local-variable stack, meaning that end will become more complicated anyways. So the landscape is changing in a way that suggests the decision should be reevaluated, and this proposal is the first sign of that change.

[tebbi]

These type annotations increase binary size and mean more work for validation, but I don't see any clear benefits. In a fast single-pass compiler, you probably want to do validation together with code generation anyway, meaning the information in these immediates is available anyway. For a slower, optimizing compiler used for tier-up, this information could be cached or should be cheap enough to re-compute. For an interpreter working directly on the wire-bytes, it could in principle be helpful to have this type information right there, at least for some operations. But the Wasm binary format is already hard to interpret without additional sidetable information, and what you really want in an interpreter is often platform-specific, like real offsets in the case of Wasm GC object access. So this information needs to be put in a sidetable or engine-specific internal bytecode anyway. So I really can't imagine any situation where these immediates would be useful enough to pay for the increased size in the transport format, especially since this is a price paid by all users independently of the respective engine even profiting from it.

[taralx]

For those like me who are curious about the history, this pull request appears to be where the blocks got types. It seems like the primary concern at the time was knowing how many stack items are retained by a branch ("arity").

[RossTate]

Thanks, @taralx! Historical context is always super useful, and expect everyone involved in that conversation appreciates being saved from repeating the conversation 😄 Looking through it, it seems the option I am suggesting was never discussed: every block-like construct (i.e. has an end) specifies an arity to know how many values to leave on the stack (I suspect 0 is extremely common), and if the block-like construct provides a branch target (e.g. block, if, and loop) then specify a "label" type for the target (e.g. [i32, i32]). Now, given what already exists, it might just be easier to say that block-like constructs providing a branch target use block types, and those not providing a branch target (like let) use an arity. But we should try to reduce how much we rely on the compression granted by using type indices—as WebAssembly's type system grows there will be fewer and fewer identical block types within a module.

[rossberg]

To clarify, let is consistent with other block constructs and binds a label -- as mentioned elsewhere, treating all block constructs uniformly as branch targets was the group's decision long ago.

That's implicit in the typing rule as stated in the proposal, though it may not be super-obvious. I added an explicit note (and fixed a bug on the way :) ).

[RossTate]

Yes, I understand let currently binds a label solely due to a decision made long ago when all block constructs naturally bound a label. Above I gave reasons to revisit that decision. Could you link to the relevant discussion behind that decision so that we can see if/how its rationale carries over to let and other non-control-flow constructs (in addition to the one linked above, which I've already tried to incorporate into the discussion here)?

[rossberg]

Unfortunately, there are no notes of that, as far as I'm aware; it was early times.

FWIW, I argued against that choice at the time, and explicitly raised the question whether this should then apply to all block constructs that we may add in the future. The resolution was yes, because otherwise the primary motivation (simplicity of decoders and validators, avoiding a separate stack for tracking labels) would have been moot.

That doesn't mean that we can't revisit, but none of the technical arguments to do so are specific to let. So such a discussion would probably deserve a more general topic and any resolution should consistently apply to all relevant block instructions. I would hence prefer to separate this particular discussion from the current proposal. Focus helps progress.

[jakobkummerow]

+1 to not requiring redundant type immediates for new instructions, in the interest of saving module size. Obviously, instructions that create new values must know a type for them; whereas instructions that consume stack values don't need to encode the expected type of these values.

From an engine implementation point of view, redundant type immediates only make us do more work at validation time, because equivalence of actual stack value type and expected type (per immediate) must be checked. Having the immediates provides no (performance or simplicity or safety) benefit. (Direct wire-byte interpreters might be an exception to this "no benefits" statement, but (1) as @tebbi explains above even that is unclear, and (2) it's also unclear whether that's the implementation strategy that Wasm should optimize for -- wouldn't most users of most engines expect to get the speed that comes from compilation to machine code?)

From a language point of view, I can see that such additional "consistency checks" might be helpful for a human-written language, but they seem significantly less useful for a compilation target.

(For background, I'm mostly looking at this from the GC proposal's perspective, but it's a design decision that should ideally be consistent. For example, struct.get could skip its type parameter and only have a field index, the semantics being "retrieve the n-th field from whatever struct is currently on top of the value stack; fail to validate if that struct doesn't have enough fields". In this proposal, ref.as_non_null could easily be polymorphic and simply return a non-null reference for whatever nullable reference type it found on the stack.)

[lars-t-hansen]

One argument in favor of out annotations on block-like structures is that in a situation where the block leaves multiple values on the stack on the way out, a streaming compiler can pre-allocate space for those values to go into (they won't all fit in registers). As it is, our baseline compiler does not make use of that information and instead ends up emitting a fair amount of data shuffling code in some cases. I probably believe that it would be possible to get rid of that shuffling code if we can know something about how much space will be required along the exit edge from the block.

I don't know that this is a particularly strong argument for us, because it's a baseline compiler - some inefficiencies are to be expected - and because I've not done the detailed analysis, nor am I likely to. I guess there could also be streaming compilers that are not quite so simplistic and would benefit more from information up-front.

[RossTate]

Hmm, interesting idea. But I suspect you'll have to have a bunch of shuffling code with that anyways. That is, even if you preallocate the space, you don't know which instruction outputs end up going into which spots until you reach the end of the block, so either you'll have to add shuffling code or you'll have to backpatch the code, which is probably what you would have done anyways 😕

But now that I understand where @rossberg meant to go with this post (sorry for the confusion, though the opening arguments do apply just as easily to block-like instructions), and that the pull requests for the relevant changes are in progress, it's probably best to let him close the issue when those are done and I'll open up another one to discuss the topic of annotations for blocks elsewhere.

[binji]

it's probably best to let him close the issue when those are done and I'll open up another one to discuss the topic of annotations for blocks elsewhere.

Sgtm, I'd suggest the design repo, since this could be a separate proposal.