3 ms·

WASM is a typed bytecode format where the stack state must be validatable at compile-time, guaranteeing that no validated program can mess up the stack at runti

by brabel 7y ago

WASM is a typed bytecode format where the stack state must be validatable at compile-time, guaranteeing that no validated program can mess up the stack at runtime. Having unstructured control flow would make it pretty much impossible to do that, wouldn't it?

__s 7y ago
Not impossible, as in the JVM there'd be a pass which verifies that the stack usage is deterministic along all program paths. It's nice not having to do that verifying step, but stack usage still has to be checked anyways, so whether it's actually a win is debatable
abecedarius 7y ago
Nah. I made a low-level VM in 2001 similar to this funclets proposal cwzwarich linked to (Hi, Cameron), and verification was a fast local check. Each funclet had a signature, you collect the signatures before you start verifying the code, and then track changes to the stack as you walk through the code, using the signatures for the effects of any calls you encounter, and finally insisting that the funclet match its declared effect. Control flow within a funclet is reducible. (I didn't call them funclets, but it sounds like the same basic scheme on glancing through. One simplification: my VM could loop only through the tail calls.)
cwzwarich 7y ago
To get linear time validation, you need conditions at each control flow transfer that can be checked locally but together imply that stack usage in the function is well-formed. The funclet approach (in more ordinary terminology) is to ensure that the stack difference from function invocation upon entry to a basic block is the same across entries to that basic block, and that those additional stack entries all have the same (statically specified) type in each invocation. This is very natural when generating code from an SSA optimizer. Java bytecode traditionally didn't contain any of this branch target or type information, and required the bytecode verifier to do an iterative combined control/data-flow analysis. Even now that they added some of that type information with stack maps, it's still more complicated than it needs to be due to the historical legacy of this approach.
int_19h 7y ago
Completely unstructured, yes. However, there are many stack-based VMs with both gotos and verification. Generally speaking, the constraint is that for any label that is a jump target, the stack must have the same count and type of elements for all possible origins. It's not hard to verify.

by brabel 7y ago

__s 7y ago

Not impossible, as in the JVM there'd be a pass which verifies that the stack usage is deterministic along all program paths. It's nice not having to do that verifying step, but stack usage still has to be checked anyways, so whether it's actually a win is debatable

abecedarius 7y ago

Nah. I made a low-level VM in 2001 similar to this funclets proposal cwzwarich linked to (Hi, Cameron), and verification was a fast local check. Each funclet had a signature, you collect the signatures before you start verifying the code, and then track changes to the stack as you walk through the code, using the signatures for the effects of any calls you encounter, and finally insisting that the funclet match its declared effect. Control flow within a funclet is reducible. (I didn't call them funclets, but it sounds like the same basic scheme on glancing through. One simplification: my VM could loop only through the tail calls.)

cwzwarich 7y ago

To get linear time validation, you need conditions at each control flow transfer that can be checked locally but together imply that stack usage in the function is well-formed. The funclet approach (in more ordinary terminology) is to ensure that the stack difference from function invocation upon entry to a basic block is the same across entries to that basic block, and that those additional stack entries all have the same (statically specified) type in each invocation. This is very natural when generating code from an SSA optimizer. Java bytecode traditionally didn't contain any of this branch target or type information, and required the bytecode verifier to do an iterative combined control/data-flow analysis. Even now that they added some of that type information with stack maps, it's still more complicated than it needs to be due to the historical legacy of this approach.

int_19h 7y ago

Completely unstructured, yes. However, there are many stack-based VMs with both gotos and verification. Generally speaking, the constraint is that for any label that is a jump target, the stack must have the same count and type of elements for all possible origins. It's not hard to verify.