Clarify that wasm may be viewed as either an AST or a stack machine.

[sunfishcode]

This PR just adds some additional introductory information. Any given document needs to pick one perspective, but it is useful to acknowledge other commonly-used perspectives to explain how they relate.

[ghost]

It may well be more efficient for the encoding to take advantage of implicit conversions and/or to specialize the operators based on the argument types with the post-order encoding. I don't see the rationale for excluding these options.

[sunfishcode]

This is preexisting text that this PR is just moving, so I'd like to suggest raising this question in a new issue.

[rossberg]

I think this is where we want to go, but it's probably premature to add this text. So far, we haven't fully demonstrated the stack machine interpretation, and in fact, until we decide to have explicit drops, it doesn't actually hold.

[ghost]

@rossberg-chromium It's not clear that drop is necessary to make it a stack machine? We already have block which unwinds the stack. I thought an issue was that operators could consume only one value per AST node to have a value stack rather than node stack interpretation, that node with no values could not be consumed.

Some stack machine code does not translate simply to an expression and I think the difference is enough that a stack interpretation does not have a clear parallel in an AST without some significant restrictions on the stack code. For example:

...
i32.load
dup 0
i32.add

I think we do need this dup operator as it helps avoid using local variables and seems consistent with SSA. The above could be encoded as follows which would have a simple expression parallel:

...
i32.load
dup 0
dup 1
i32.add

(let (($v1 (i32.load ...))
      ($v2 (i32.add (get_value $v1) (get_value $v1)))
      )
  )

The restriction here is that values popped must have only one use in order for them to have a simple expression parallel, and values used multiple times would be let block top level expressions and not popped until the end of the block. Would we want to validate such a restriction, or choose a more flexible stack machine code - perhaps a choice needs to be made and they are not parallel interpretations, or perhaps some other encoding can capture the single use pattern efficiently without needing a stack machine.

[sunfishcode]

@rossberg-chromium I've found it useful to be able to think about wasm as a stack machine for several months now. As someone who has done would I hope can be considered relevant work on both the producer and consumer side with the help of this interpretation, I can confirm that it does hold, with or without explicit drops, multi-value, void, any, invalid, empty, or other details.

[lukewagner]

In particular, w/o the explicit drop, you have to pretend that all void-returning operators push a special "void" value.

So lgtm and this matches how I've been looking at things too.

[rossberg]

@lukewagner, I didn't count that as a proper stack machine interpretation (as you guys said, it's weird), but fair enough.

LGTM

[kripken]

Is the second part of this sentence true? How does each node represent an instruction in a typed stack machine, for if_else for example?

[sunfishcode]

In the 0xb encoding, if_else was split into if, else, and end. In a stack-machine interpretation, these each become independent opcodes that each have a well-defined effect in terms of the value stack and the control flow stack.

[binji]

Isn't this like forth's IF ELSE THEN?
@flagxor?

[kripken]

Can you please elaborate on what those "well-defined effects" are? I'd like to understand this, and it isn't obvious to me. I remember we talked about this a long time ago, and there wasn't a simple answer - has that changed? Or is my memory wrong? :)

[binji]

Well, you can take a look at the implementation here: https://github.com/WebAssembly/sexpr-wasm-prototype/blob/master/src/wasm-binary-reader-interpreter.c#L1247. It converts from wasm opcodes to a very similar stack machine, but with gotos instead of structured control flow. IF becomes BR_UNLESS, ELSE becomes a BR and a branch fixup for BR_UNLESS, and END does a branch fixup of the BR.

The only other slightly tricky part is determining whether the result of the expression needs to be discarded. With the current opcodes, that must be done in a prepass.

[kripken]

I see, thanks.

[kripken]

I see the value in this information, but I believe it's being added to the wrong place. @sunfishcode, you mentioned that in 0xb things are as they are, but that's the binary format - this page is about the abstract operations and types and so forth. Your stack machine interpretation is for the binary format, so having it in AST semantics is misleading.

Specifically, when you say "form" in the first sentence, you mean "binary format", but we shouldn't talk about the binary format - nor the text format, for that matter - in the AST semantics document.

[lukewagner]

I think the placement makes sense since the comment pertains to both the AST and semantics and for someone new to wasm who shows up at this doc (which is sortof the nexus of the whole repo), if they have any familiarity with stack machines, it could help them establish context.

[kripken]

As the nexus, I agree it makes sense to mention this and refer to the binary format doc for more details. Perhaps something like "For simplicity we define and describe these semantics in terms of an AST. VMs can implement these semantics in various ways, for example as a concrete AST, a stack machine (see more details in BinaryFormat), or something else."

[sunfishcode]

@kripken The stack machine approach to semantics can be a pure abstraction the same way the AST is. It can describe how WebAssembly works, independently of how it's encoded. The postorder encoding makes the mapping to the binary format much more obvious, but the mapping was always there. For example, I wrote some code which found these concepts useful well before the switch to postorder happened.

I'd prefer to avoid adding "for simplicity" because I happen to think the stack machine semantics are simple too, overall -- simpler in some areas and more complex in others.

VMs can implement these semantics in various ways, for example as a concrete AST, a stack machine (see more details in BinaryFormat), or something else.

Does this sentence:

"Implementations need not build an actual AST or maintain an actual stack; they need only behave as if they did so."

cover that? I'd prefer to avoid linking to BinaryFormat.md here, because the stack machine concept exists independently of any particular encoding.

[ghost]

@sunfishcode I agree that a stack machine could define the AST semantics, but at present it strictly does not. There are strictly stack machine codes that do no translate to the current AST semantics. So what you are staying is just that the AST can be compiled to a stack machine, but it can also be compiled to an expressionless encoding or to machine code and these could also define the AST semantics but they do not at present either.

Stack machines generally do not represent zero-value stack entries, rather they would just not have a stack entry if there were no value, and also multiple values are generally pushed to multiple stack slots. Take a look at the sexp-wasm stack machine - the wasm AST is compiled to this stack machine. You would need to demonstrate a trivial lossless translation from this stack code back to the AST for them to be equivalent?

Part of the problem is that 'stack machine' is not defined. People once called a language with a call stack a stack machine, and wasm has a call stack, but does that make it useful to describe it as a stack machine? No one can argue against the description because it is effectively defined as 'a stack machine restricted to match the AST semantics', which is just a product of the one way compilation to a stack machine, but how does that help the reader without defining the necessary restrictions? How does the reader translate from their general understanding of a stack machine to the AST representation of this?

I gave one challenge above using dup. Here's another piece of stack machine code that has no AST representation:

call_returning_two_values
i32.const 1
call_with_three_args

And another using drop:

call_returning_const_1
call_returning_const_2
drop
i32.eqz

And another:

call_returning_const_1
call_returning_no_values
i32.eqz

[sunfishcode]

@kripken I reworded the paragraph along the lines we discussed offline. Does this work?

[kripken]

I would put the "In practice" sentence in parens, as this document is not about implementation details. I agree it's worth mentioning, just it's an aside for clarification purposes, and as such, parens seem suitable.

[kripken]

"it is also possible to X" suggests X is the only alternative. is it?

instead, how about "however, it is also possible to understand WebAssembly semantics in other ways, for example, in terms of a stack machine".

[kripken]

Thanks, looks a lot nicer imo :) Still I have some comments. Sorry for all the details, but as @lukewagner said, this is a central page and every word counts.

[sunfishcode]

@JSStats Yes; there are several semantic restrictions on the stack machine. Also, stack machines can be built to handle void types, or not, tuple types, or not, dup instructions, or not, and any number of other variations or restrictions. These are interesting details for wasm, but they don't change the overall observation being made here.

@kripken Added parens and removed "typed". I kept the "it is also possible to X" there though. There are obviously many other ways one could describe wasm semantics, but stack machines aren't just one example among a crowd of theoretical alternatives: they're an important concept that's contributing to the overall WebAssembly design effort.

[kripken]

Thanks, lgtm.

[sunfishcode]

Merging with lgtms.