Stream: wasm

Topic: Is function-local stack space always unbounded?

James (Aug 02 2022 at 06:48):

I'm wondering if it's possible for there to be unbounded operand stack usage within WebAssembly code.
Closest I could think is loops, which doesn't exactly happen:

(func
  loop (result i32)
    i32.const 5
    br 0
  end
  unreachable)

The above example will implicitly pop the 5 before branching.

(func
  i32.const 6
  loop (param i32) (result i32)
    i32.const 5
    br 0
  end
  unreachable)

The above example will implicitly copy the 5 before branching, and pop the 6. (making the stack look like 6 5 on the first loop, then 5 5 on all subsequent branches)
I'm wondering if there's any edge-cases where unbounded stack usage can happen.
By unbounded, I don't include recursion. I mean unbounded with respect to the current call frame (not including any sub-calls' frames)

Mario Carneiro (Aug 02 2022 at 08:32):

No, stack space is bounded. I was hoping it would be a consequence of the soundness theorem, but I don't see an obvious way to get it. Instead, you can argue as follows:

1. Suppose there is an execution of a function which consumes unbounded stack space. Then it must go through infinitely many configurations and execute infinitely many instructions.
2. There are a finite number of labels in the execution of a given function. This isn't obvious from the WASM specification, but it follows because there are a finite number of continuations corresponding to suffixes of the program, and each label is determined by a block type (which is associated to some instruction from the original source, so finite) and a continuation.
3. Without loops, the program would halt, so the loop instruction must be used, and in particular one of the finitely many labels must be traversed infinitely many times (and with different configurations, because otherwise the whole program would recur and not use unbounded memory).
4. The loop starts with this operation:

$$F; \mathit{val}^m~\mathsf{loop}~\mathit{bt}~\mathit{instr}^\ast~\mathsf{end} \hookrightarrow F; \mathsf{label}_m\{\mathsf{loop}~\mathit{bt}~\mathit{instr}^\ast~\mathsf{end}\}~\mathit{val}^m~\mathit{instr}^\ast~\mathsf{end}$$

and the label blocks the stack below it until it is jumped to in this operation:

$$\mathsf{label}_m\{\mathsf{loop}~\mathit{bt}~\mathit{instr}^\ast~\mathsf{end}\}~B^l[\mathit{val}^m~(\mathsf{br}~l)]~\mathsf{end} \hookrightarrow \mathit{val}^m~\mathsf{loop}~\mathit{bt}~\mathit{instr}^\ast~\mathsf{end}$$

But this is a problem, because the state $\mathit{val}^m~\mathsf{loop}~\mathit{bt}~\mathit{instr}^\ast~\mathsf{end}$ at the end of the second transition is exactly the starting state of the first transition. That means that if $S$ is the upper part of the stack, we will always either have $S,\mathit{val}^m~\mathsf{loop}~\mathit{bt}~\mathit{instr}^\ast~\mathsf{end}$ or $S,\mathsf{label}_m\{\mathsf{loop}~\mathit{bt}~\mathit{instr}^\ast~\mathsf{end}\},\dots$ in this loop, where $S$ is fixed and inaccessible. So we can't get an infinite number of different stack shapes; the only state we have to work with is the $\mathit{val}^m$, where $m$ is predetermined from the block type of the loop label.

Mario Carneiro (Aug 02 2022 at 08:35):

An alternative proof is: it's intended to run on regular hardware via standard compiler analyses, so of course the size of the stack frame is statically determinable, else the spec would be broken.

James (Aug 03 2022 at 01:15):

Thanks. Yeah, I realized that it would be pretty much impossible to determine the stack's validity with respect to its operands, if it were able to use unbounded space, since the only real operations where that could happen would likely have to be dependent on the value of the operand put in, which is not allowed by the spec--WASM instructions can be dependent on the stack's current type, but not dependent on values within the stack (this would end up having more of a... dependent type system which would be kind of infeasible to check in the general case within a reasonable amount of time and with a reasonable amount of simplicity).

Last updated: Nov 22 2024 at 16:03 UTC