Skip to content

Implement basic support for sockets #3449

Open
@RalfJung

Description

@RalfJung

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-filesArea: related to files, paths, sockets, file descriptors, or handlesA-shimsArea: This affects the external function shimsA-unixArea: affects our shared Unix target supportC-projectCategory: a larger project is being tracked here, usually with checkmarks for individual steps

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions