What is the role & scope of type checking in stack switching?

[fgmccabe]

Type checking, in general, is a technique for allowing limited correctness proofs for programs. For high-level languages this typically revolves around the allowed values a variable may be assigned to and the allowed uses of variables.

For a virtual machine like WebAssembly, the goal has a different focus: we need to ensure that the machine cannot enter an invalid state. One important feature of this viewpoint compared to that of high-level languages is that the machine cannot trust the output of a compiler. Or, perhaps more accurately, the machine has to be able to verify that its integrity will not be compromised.

For stack switching, this may seem straightforward: there must be sufficient metadata available to ensure that a stack switch cannot violate integrity constraints of the engine. Furthermore, if this could be proved when compiling the module this must be better than if the machine has to keep re-proving the safety. However, in many applications of stack switching, even if the types involved in a stack switch could be proved statically, it is also often necessary to use cast instructions to allow the program to 'prepare' for a stack switch -- i.e., loading the target to switch to can also involve executing a cast instruction.

[dead-claudia]

I feel substructural types would help, though they wouldn't need to be specified explicitly. Specifically, here's how I could envision this being encoded at a high level:

• Stack items must be consumed exactly once, and in the reverse order they are defined.
  • Define: push the item
  • Use: pop the item, optionally to use its inner value
• Stacks can be consumed at most once, but in any order.
  • Define: one of the following
    • Create a new empty stack
    • Get the current stack, switch to parent stack, pop old parent stack
  • Use:
    • Switch to stack
    • Push old parent stack, set parent stack to current stack, switch to specified stack

There are already some implications here:

• By having the call consume the old stack and return the new stack, it's strictly impossible to even represent a situation where stack integrity could be violated through the use of stack variables alone.
• When reading it from a persistent location (whether it be a local, a table, or even a GC cell), the old reference must be invalidated, and invalidated references must trap upon attempts to use. This is critical to enforce at runtime the invariant of it being consumed at most once.
  • This also means local.get cannot be a stateless action when it comes to retrieving stacks. Implementations of course can optimize that check out in most cases, and JIT-compiling ones already do the analysis needed to detect such cases so they can allocate registers better.

As for how the types would work out:

• A suspendable version of (func ...) would need added, with two extra groups: a list of suspend results and a list of resume parameters.
• stackref t - A nullable reference to a stack. This can be used anywhere a generic ref type is accepted or returned, and it can even be dropped, selected, and similar as usual.
  • t is a reference to the relevant suspendable function type (see above).
• local.get, global.get, and table.get, when returning a value of type stackref, must additionally set its previous value to ref.null stackref t.
• local.tee cannot be used for values of type stackref t.

[RossTate]

Indeed substructural types have been explored in this design space. The feedback was that they introduced more complexities than their advantages merited (for this design space). For example, how should an engine implement clearing the entry of a shared table after a get in a multithreaded setting, particularly if stackref or contref is wide (which is currently being discussed as a possibility for the latter to reduce memory allocations)?

[dead-claudia]

@RossTate That's fair regarding fat pointers, though I will note that I only proposed a stackref. Also, I do want to call out one thing: one could make my stackref here thin by pushing the resume info (instruction pointer, base pointer, pointer to global offsets, etc.) onto the stack before switching and just using the stack pointer itself as the pointer. In theory, this requires extra data to be allocated, but in practice the stack is likely to have enough free space to make it near zero-cost to use anyways (we're talking like at most a few pointers), and if a red zone exists, this could just use that to save and restore state.

[rossberg]

Unfortunately, statically tracking linearity would be quite a bit more complicated than that, since stackrefs are first-class values (and need to be), so you can and want to pass them to other functions, store them in globals or other data structures, etc. Typing disciplines for this have been explored widely in the literature, but in practice, they are complex and very difficult to target. You'll need notions like borrowing to make them expressive enough, and even then you are bound to bump into serious expressiveness limitations, as e.g. witnessed by the frequent occurrence of unsafe in low-level Rust libraries.

[dead-claudia]

Typing disciplines for this have been explored widely in the literature, but in practice, they are complex and very difficult to target. You'll need notions like borrowing to make them expressive enough, and even then you are bound to bump into serious expressiveness limitations, as e.g. witnessed by the frequent occurrence of unsafe in low-level Rust libraries.

That is true. I was hoping to punt this complexity from validation time to runtime by simply having stackref loads null out their source operand, in hopes that implementors could optimize that out in common cases. This of course does carry concerns around performance, especially when using linear memory for stacks, and so I could see this as a non-starter for some.