Stacks Design

[RossTate]

As requested, here is a write-up of the design I mentioned in my presentation (WebAssembly/meetings#934).

Overview

The idea of the design is to give wasm programs access to first-class stacks as a low-level resource (though abstractly enough for engines to implement in a variety of ways), with which they can directly support features such as lightweight threads or (delimited) continuations or (deep/shallow) (uni/bi-directional) algebraic effects. At the same time, the design is mindful that not all stacks can/should be safely treated so flexibly (e.g. host stacks or C stacks), and that stack switching should not be able to bypass control invariants that the embedder or other programs rely on.

Design

The First-Class-Stack Type

stack_extend $struct_type $label_type $label_type+

First-class stacks can have a number of fields at the root of the stack, the layout and types of which is specified by $struct_type. (Engines using a simple GC might implement this by having a regular GC struct with the given fields plus a pointer to a stack without fields.)

Every first-class stack is in one of two states:

• Mounted
  • In this state, the first-class stack has a pointer to a "parent" stack (which may or not be a first-class stack) that is configured to be returned to an instruction whose input is the given $label_type.
  • In this state, the first-class stack also has a boolean field indicating whether it is "concealed" or not.
• Suspended
  • In this state, the first-class stack is configured to be resumed to a choice of labels whose types are given by $label_type+

A stack is "suspendable" if it is a mounted first-class stack that is not concealed.

Note: Some surface languages that have features like delimited continuations that would natively be implemented using stacks, each with a notion of parent. The "parent" above is for cross-application composition of control (e.g. making sure that a JS or a C++-to-wasm application can call a function imported from a Racket-to-wasm application and expect normal return, rather than Racket's stack-switching being able to bypass the caller's stack). So such languages are expected to include an application-level "parent" field in the $struct_type of its stacks, manually implementing their particular semantics for features like delimited continuations, just as they would in a native implementation.

The stack type of a function/instruction

Function types are extended to have an optional stack $heap_type specifier (alongside the optional param and result specifiers).
This specifier indicates that if the stack that the function's call frame is on is suspendable, then it has type $heap_type.

Instructions of the function are type-checked with $heap_type as the stack type.
Such instructions can have no stack type, or can have a stack type of any supertype of $heap_type.
Function-calling instructions have the stack type of the function they are calling.

Allocating Stacks

stack.new $stack_type $func+ : [tf* ti*] -> [(ref $stack_type)]

• where $stack_type = stack_extend $struct_type $label_type $label_type+
• tf* are the values needed to initialize $struct_type
• the result type of each function in $func+ is a subtype of $label_type
• the param type of each function in $func+ is a supertype of each corresponding label type in $label_type+ prepended by [ti*]
• when present, the stack type of each function in $func is a supertype of $stack_type

Creates a new suspended first-class stack that, when resumed with a particular label index, will call the corresponding $func with the given ti* and the values used to resume the stack.
Whenever the function eventually returns, the stack will be dismounted (see below) using the given values.
If the function ever traps or throws an exception, the stack will be dismounted (see below) and the trap or exception will be propagated from the resumption point of its parent stack.

Mounting and Dismounting Stacks

stack.mount n : [ti* (ref $stack_type)] -> [to*]

• where $stack_type = stack_extend $struct_type $label_type $label_type+
• the nth element of $label_type+ is `[ti*]
• $label_type = [to*]

Traps if the given first-class stack is not suspended.
Changes its state to mounted (and not concealed), sets its parent as the current stack, and transfers control to its nth resumption label using the [ti*] values.
Note: does not have a stack type and does not require the current stack to be suspendable, meaning it successfully executes on any stack.

stack.dismount $label+ : [ti*] -> unreachable (stack $stack_type)

• where $stack_type = stack_extend $struct_type $label_type $label_type+
• $label_type = [ti*]
• the type of each label in $label+ is a supertype of the corresponding label type in $label_type+

Traps if the current stack is not suspendable.
Changes the current stack's state to suspended, with the specified labels as its resumption points.
Transfers control to the parent stack using the [ti*] values.

Switching Stacks

stack.switch n $label+ : [ti* (ref $to_stack_type)] -> unreachable (stack $from_stack_type)

• where $from_stack_type = stack_extend $from_struct_type $from_label_type $from_label_type+
• where $to_stack_type = stack_extend $to_struct_type $to_label_type $to_label_type+
• $from_label_type <: $to_label_type
• the nth element of $to_label_type+ is [ti*]
• the type of each label in $label+ is a supertype of the corresponding label type in $from_label_type+

Traps if the current stack is not suspendable or the given stack is not suspended.
Changes the current stack's state to suspended, with the specified labels as its resumption points, after copying its parent to the given stack, which becomes mounted (and not concealed).
Transfers control to the given stack's nth resumption label using the [ti*] values.

Calling Variations

stack.mount/dismount/switch each have a ..._call $func variation wherein, rather than transferring control to the target control point, that control point is instead used as the return address for a call to $func using the given values.
As an important example, $func can use the given values to simply throw an exception, which will be thrown from that control point, which makes ..._throw variants of these instructions unnecessary.

Examining and Concealing Stacks

stack.current : [] -> [(ref null $heap_type)] (stack $heap_type)

Returns the reference to the current stack if it is suspendable, and otherwise returns null.

This, in combination with the fact that a stack type can have custom fields, is useful for implementing green-thread-local storage and for supporting dynamic scope in languages with delimited continuations.

stack.conceal $heap_type instr* end : [ti*] -> [to*]

• where instr* : [ti*] -> [to*] (stack $heap_type)

If the current stack is not concealed, then makes it concealed, executes instr*, and unconceals it afterwards (or if an exception is thrown).
Note: while stack.conceal has no stack type, instr* can have the specified heap type.
This is sound for any heap type because stack.current will always return null since the current stack is necessarily not suspendable during the execution of these instructions.

This design ensures that imported functions without a stack type cannot access or transfer control out of the current stack of the caller, while at the same time also allowing one to call functions with a stack type that the caller does not have (by wrapping the call with stack.conceal).
These design points are particularly useful for the JS API.

Advanced Instructions

Instructions for adding frames to a stack or duplicating a stack might be useful for some applications.

JS Interop

When converting a JS function to a WebAssembly function that specifies a stack type, the stack type is ignored entirely (because the JS function makes no use of the current stack).

When converting a WebAssembly function that specifies a stack type to a JS function, the JS wrapper essentially calls the WebAssembly function inside a stack.conceal.

Tooling

The above design means you can add a chosen stack type to all function types in the types section, and the resulting WebAssembly module will type-check and validate just as before, and it will interop with JS just as before. If you have multiple WebAssembly modules that are calling each other's functions, just perform this pass through all of them using the same chosen stack type, and they'll interop just as before as well.

Properties

This has the abstraction/security properties of "lexical" effect handlers, including ensuring that JS code cannot be suspended. It also guarantees that there's always a dynamic scope for traps/exceptions (and there's no way to bypass an unsuspendable caller's trap/exception handlers).

[fgmccabe]

Thanks for this