Block-type annotations for branch-unrelated block-like instructions are redundant

[RossTate]

Originally, and I believe still currently, all block-like instructions—meaning instructions with a matching end such as block/if/loop—in WebAssembly introduce a branch target. For efficient type-checking, it is important that the type of this branch target be annotated. To this end, block types were introduced. Originally block types were restricted, but those restrictions were lifted in the Multi-Value proposal.

But as WebAssembly grows, there will be more block-like instructions, and many will not be naturally related to branching. The first example on the horizon is let in the Typed Function References proposal. This instruction simply binds stack slots to fresh local variables that remain in scope until the matching end instruction.

Currently, let has a block-type annotation and introduces a branch target in order to be consistent with the existing block-like instructions whose purpose all happen to be to introduce branch targets. If we eliminate the feature-unrelated branch target of let, then its block-type annotation is redundant and is counter to one of let's main values: reducing type annotations. As discussed in the recent CG meeting, redundant type annotations not only increase binary size—they actually even slow down validation. As the type system gets richer, these downsides will only worsen because it will take more space to describe redundant type annotations (and it will be less common for type annotations to overlap) and it will take more time to validate redundant type annotations.

There seemed to be widespread support for removing redundant type annotations from non-block-like instructions, so here I wanted to discuss removing them from upcoming block-like instructions. There are three degrees to which this can be done, and I recommend getting consensus on each degree in order before proceeding to the next:

1. Do not require redundant block-type annotations, e.g. on naturally control-unrelated instructions like let.
2. Only require label-type annotations on unreleased control-related block-like instructions, e.g. try.
3. Only require label-type annotations on released control-related block-like instructions: block/if/loop.

Regarding Degrees 2 and 3, in all of block/if/loop/try, only half of the block-type annotation is helpful: the half that you can branch to. For the other half, you only need to specify the number of operands to leave on the stack. But, as I said, it's best to defer discussion of this more complex issue until after the easier issue (Degree 1) has been resolved. I just wanted to mention this here because it's likely to come up in the discussion anyways, if only to explain why certain annotations are unnecessary, and because all the discussion of Degree 1 will be relevant to Degrees 2 and 3 and it would be jarring to start a completely new issue for those with much of its relevant context here. I'll update the following status as appropriate:

Status: Only Degree 1 in discussion. Please share your thoughts and assume all comments are within the scope of Degree 1 unless otherwise stated!

P.S. If you're wondering how the block-type annotation for let can be redundant, the "principal" input stack-type of a let block is the output stack-type of the previous instruction (minus whatever stack slots let binds to fresh local variables), and the "principal" output stack-type of a let block is the output stack-type of the last instruction of the block's body. Adding a block-type annotation would just add more steps to the type-checker: check that the output stack-type of the previous instruction is a subtype of the annotation's input stack-type, type-check the body using just the annotation's (weaker) input stack-type, check that the output stack-type of the last instruction of the block's body is a subtype of the annotation's output stack-type, and type-check subsequent instructions using just the annotation's (weaker) output stack-type.

[taralx]

I'm in favor of degree 1. Feel free to add reacts to this message if you just want to agree.

[rossberg]

To be clear, this question is not primarily about type annotations, but whether block instructions should be labelled, i.e., valid as jump targets.

To reiterate the historic context: There was extensive discussion about this question in one of the early design meetings for Wasm (no notes of that, unfortunately). At the time, the group's decision was to treat all block-like constructs (current and future) as labelled. IIRC, the two main arguments were: (1) it simplifies decoders/validators if control stack and label stack can be the combined; and (2) it may save an extra block in some cases. The only counter argument was that the semantics of block instructions is somewhat more complicated with labels.

However, that was before we introduced type annotations on blocks, so now the code size / checking time argument might work the other way. However, point (1) still stands, and with it the broader argument of uniform treatment of all blocks. Uniformity ultimately simplifies both semantics and implementations overall.

Before deciding to break this I would urge to get some measurements demonstrating significant code size or validation time improvements on realistic programs. Given that none of these instructions are likely to be hot in practice, it might simply not matter.

[RossTate]

(1) it simplifies decoders/validators if control stack and label stack can be the combined

"Control" stack is a bit of a misnomer here. Syntactic stack is more accurate; it's the syntactic nesting of blocks. And yes, I could have phrased the question as "should all syntactic nesting blocks be made into control blocks even if they're primary functionality is unrelated to control".

Given that clarification, let introduces a need to maintain a stack of locals, separate from the syntactic stack, anyways. This requires a pretty minor change to the architecture of the interpreters: when you pop an element off the syntactic stack, you pop elements off of other stacks depending on the syntactic element that was popped. So popping let would pop elements off the locals stack, whereas block/if/else/loop would pop an element off the label stack. This architectural change also nicely extends if we add more stack-based indexing to WebAssembly. Looking at the reference interpreter, this doesn't seem to require any architectural change there.

But I believe you mentioned elsewhere that you actually disagreed with this decision anyways, and no one else else argued this in prior side discussions, which is why I elided this concern above. So I'd rather someone personally advocate for this position before we spend time discussing it.

Before deciding to break this I would urge to get some measurements demonstrating significant code size or validation time improvements on realistic programs.

This suggestion misses the point above about scaling. Right now WebAssembly has only 4 (soon to be 5) value types, and with a trivial subtyping relation to boot. Both the current Typed Function References proposal and the current GC proposal would change that to infinite value types with non-trivial (even quadratic-time in the latter case) subtyping. There is no way any measurements now of either annotation size or validation time could at all be a predictor of annotation size or validation time after these proposals.

[binji]

Both the current Typed Function References proposal and the current GC proposal would change that to infinite value types with non-trivial (even quadratic-time in the latter case) subtyping. There is no way any measurements now of either annotation size or validation time could at all be a predictor of annotation size or validation time after these proposals.

I'd guess we can use the v8 and SpiderMonkey GC prototypes, along with code generated by Kotlin/OCaml/Java as producers, to test this.

[RossTate]

Maybe? They'd still only get measurements for let, as that's currently the only applicable block-like structure that exists (for Degree 1).

What I'm wondering is what will happen if we get to stack marks, which are frequent. Consider a very simple one for stack tracing. In Python, a stack-trace entry (let's call it a code point) is a file-name string, a file-line integer, a function-name string, and a formatted-expression string. So you might imagine having something like the following to support custom stack tracing:
code_point_mark $python_cp "filename" 56 "funcname" "expr" (instr*) end

This would indicate that, while control is within instr*, the code point File "Filename", line 56, in funcname: expr is on the stack for purposes of Python stack tracing. This is part of Python's semantics: you can call traceback.extract_stack() at any point in your code and get a standardized list of these quadruples. Of course, there are tricks a Python-to-WebAssembly compiler can do to compress a given mark so that it doesn't always need 4 arguments. But what such a compiler can't do is eliminate the mark entirely.

If ever we add this functionality, these marks will be all over the place. It will be extremely rare to ever use any control-flow label associated with the mark (since that's not at all related to their purpose), and every one of their type annotations would be redundant. (And, yes, Python can be interpreted, but a number of other languages like Java and C# also have standardized stack-trace semantics.)

I have no idea if we're going to add marks, and let's not digress into debating that. The point is that there is good reason to believe that let is likely just the first example of many. And so I find it odd that there's a ruling of some sort in place to add redundant type annotations to constructs we haven't even developed yet, especially when the alternative in the worst case just surrounds the construct with a block and end instruction in total taking up 2 bytes (whereas a redundant type annotation is at least 1 byte plus the validation effort).