Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement basic support for sockets #3449

Open
RalfJung opened this issue Apr 4, 2024 · 1 comment
Open

Implement basic support for sockets #3449

RalfJung opened this issue Apr 4, 2024 · 1 comment
Labels
A-files Area: related to files, paths, sockets, file descriptors, or handles A-shims Area: This affects the external function shims A-unix Area: affects our shared Unix target support C-project Category: a larger project is being tracked here, usually with checkmarks for individual steps

Comments

@RalfJung
Copy link
Member

RalfJung commented Apr 4, 2024

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.

@RalfJung RalfJung added C-project Category: a larger project is being tracked here, usually with checkmarks for individual steps A-shims Area: This affects the external function shims labels Apr 4, 2024
@RalfJung RalfJung added A-files Area: related to files, paths, sockets, file descriptors, or handles A-unix Area: affects our shared Unix target support labels May 5, 2024
@RalfJung
Copy link
Member Author

RalfJung commented May 5, 2024

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.)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-files Area: related to files, paths, sockets, file descriptors, or handles A-shims Area: This affects the external function shims A-unix Area: affects our shared Unix target support C-project Category: a larger project is being tracked here, usually with checkmarks for individual steps
Projects
None yet
Development

No branches or pull requests

1 participant