Is it possible for Miri to support stack switching for fibers/coroutines/etc?

[alexcrichton]

Over in Wasmtime we use Miri to help verify our unsafe code isn't at least too too unsafe, but a big blind spot for us in our Miri testing right now is everything related to async. In Wasmtime all async execution of WebAssembly happens on a separate stack via a custom implementation of fibers internally. This implementation of fibers uses inline assembly on each architecture to do the actual fiber swaps/initialization/etc, but this naturally isn't supported on Miri.

Which leads me to a question: does Miri currently support stack switching, and if not is there a tracking issue or discussion to follow? If not, would it be useful to have a tracking issue? If not, no worries and I'd be happy to close this as well, but wanted to ask the question!

[RalfJung]

There is no stack switching support currently, no. The only way in which Miri has multiple stacks is by creating new threads.

How would you imagine stack switching to work in Miri? Obviously, inline assembly cannot work. Miri doesn't even have an in-memory stack the same way real code does.

What I could imagine is that Miri could provide more fine-grained operations on threads, giving "userland" control over suspension and resumption. These would still be full "heavy" threads in Miri, but could behave more like green threads from the user perspective. I don't know what a reasonable API for this could look like though -- and at least a crude approximation can probably be implemented without any new APIs, using just regular Rust threads and thread parking.

[alexcrichton]

What you're describing is roughly what I was envisioning yeah, various Miri intrinsics for a full-blown thread where the major differences to an actual thread are (a) no parallelism and (b) shared TLS variables.

One possible API to draw inspiration from would be Windows' CreateFiberEx and SwitchToFiber which Wasmtime uses here for example. I suspect that Miri might need to place some loose restrictions on usage over something like raw inline assembly where the are checked requirements about resumption/suspension in terms of hierarchies and such, but at least for our use case that would be fine. Another possible source of inspiration could be the WebAssembly stack-switching proposal.

A rough sketch of what the Windows-style API would look like is (apologies I don't know how Miri intrinsics exactly look today so I'm sort of guessing):

extern "C" {
    fn __miri_fiber_new(stack_size: usize, init: fn(*mut u8), data: *mut u8) -> u32;
    fn __miri_fiber_current() -> u32;
    fn __miri_fiber_switch(destination: u32);
}

The __miri_fiber_current would lazily assign some sort of identifier to the origin thread itself so the origin thread could be switched back to as part of __miri_fiber_switch. I haven't thought too deeply though about the implication of "spaghetti stacks" that might arise from an API such as this though.

at least a crude approximation can probably be implemented without any new APIs, using just regular Rust threads and thread parking.

Indeed! A colleague of mine had this idea as well and I'm currently in the process of implementing this so we can run more async bits through Miri in CI. So far it's working well enough to exercise more code (yay!) and I don't think we'd really need something like this feature, but that's mostly because we don't happen to share TLS variables across fibers at this time and if we did it'd be a bit of a non-starter.

[RalfJung]

A rough sketch of what the Windows-style API would look like is (apologies I don't know how Miri intrinsics exactly look today so I'm sort of guessing):

That sounds plausible, except the concept of a "stack size" makes no sense in Miri so we'd probably drop that.

Is it permitted to switch to a fiber that was created by a different thread, i.e., can fibers migrate from one thread to another?

shared TLS variables.

Ah, that does require this to be a truly first-class thing in Miri, true.

OS APIs that "get the current thread ID" would also have to be made fiber-aware.

[alexcrichton]

For Wasmtime's use case we do have situations where fibers are created one thread and migrated to another yeah, effectively due to work-stealing that Tokio does. Now that's all high-level performance optimizations though which we can exclude in testing so it shouldn't affect us too much one way or another, but that's at least our use case for it.

For stack size though would Miri want to use it as a rough approximation of a stack overflow? For example if a fiber is created with 2x more memory you could have 2x more recursion? The actual number would be sort of meaningless but might be a rough proxy to how deep recursion is allowed to go.

[RalfJung]

The Miri stack lives outside of memory, only the actual local variables live in memory. There they share one pool with all other allocations (heap, globals, everything).

"Stack overflow" is not a thing in Miri. "Running out of address space" could be a thing, though is unlikely. The most likely thing to happen is that Miri itself runs out of host memory to allocate for the target program it runs.

[alexcrichton]

Ah ok yeah that makes sense, and also explains why the stack overflow test I accidentally ran in Miri took so long... Good to know!