RalfJung
commented
2 months ago As discussed on Zulip, it would probably make sense to use mio on the Miri side here. Fundamentally, the primitives we need are:
- each time the active thread yields, do a non-blocking poll on a set of host sockets -- that's generalizing what we already do here where we check whether there's a timer we need to fire
- if all Miri threads are blocked, do a blocking poll on a set of host sockets (potentially with a timeout) -- that's generalizing what we do here and here where we just sleep until the next timeout expires
The hope is that mio would give us both of these in a platform-independent way, so that we can run on Windows hosts. (Note that this issue is only about Unix targets, using the typical POSIX socket API. Support for sockets on Windows targets is out-of-scope here. But if possible we should support running Unix targets on Windows hosts, as we already do with file system access.)
Miri can access files but not sockets currently.
The main issue with implementing blocking sockets is that they would provide the first source of blocking in Miri that is controlled by the outside world (except for time but we've got that handled pretty well). That will be quite non-trivial to implement as Miri needs to basically become or import an async runtime. We'll have a concept of threads being blocked on a socket. When all threads are blocked and Miri goes to sleep to wait for a timeout to pass, it needs to be able to wait on "either the timeout passes or all the sockets any thread is blocked on". When the socket unblocks we should wake up the thread, even if we never reach the "all threads are blocked" state. Both of these are exactly the core operations of an async runtime.
Somewhat surprisingly, I do not think that epoll makes this a lot more complicated. Even without epoll, we could have 5 threads waiting on a different socket each, so Miri basically needs epoll on the host even if Miri programs do not have epoll available. Having epoll just means that a single Miri thread can wait on more than one socket, but since Miri anyway has to support many threads that doesn't add significant new complications.
Non-blocking sockets would be a lot simpler, but probably also a lot less interesting.