You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
RalfJung opened this issue
Apr 4, 2024
· 3 comments
Assignees
Labels
A-filesArea: related to files, paths, sockets, file descriptors, or handlesA-shimsArea: This affects the external function shimsC-projectCategory: a larger project is being tracked here, usually with checkmarks for individual steps
The epoll API mainly consists of epoll_create1, epoll_ctl, and epoll_wait. We have basic shims for all these functions but currently our epoll support is mostly a stub, since the actual polling part is still missing. (Also the behavior of dup on an epoll file descriptor is likely wrong.)
Implementing this is non-trivial, since it introduces a new kind of blocking to Miri: block until any of a set of FDs is read for reads/writes. We currently don't have any notion of file descriptors blocking at all, so this will need some careful design We probably need some notion of a per-file-descriptor wait lists of threads that are blocked on this FD? We should probably have eventfd and socketpair implemented first so that we have some examples of blocking FDs to consider.
Also note some interesting tidbits in this SO question: we may have to explicitly implement the concept of a file description as that seems to be observable through the epoll APIs. On the plus side this means we can implement dup once and for all and we don't have to rely on each and every FD type doing it correctly.
The text was updated successfully, but these errors were encountered:
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
Note that this does not require #3449, and doesn't run into the complications mentioned there regarding Miri becoming itself an async runtime. Miri can internally implement an operation blocking on N different things just fine, as long as those things are all events Miri completely controls (like socketpair and eventfd where Miri knows exactly when they are unblocked). We "just" need to find a good way to structure this so it does not become messy and can scale to more types of FDs.
Hi, I am going to work on this as potential GSoC project. Since eventfd and socketpair need to be implemented, I will work on #3442 and #3445 first. Since this also requires quite a lot of planning, I will consolidate my ideas and planning somewhere and send the link here once I cleared #3442 and #3445 .
A-filesArea: related to files, paths, sockets, file descriptors, or handlesA-shimsArea: This affects the external function shimsC-projectCategory: a larger project is being tracked here, usually with checkmarks for individual steps
The epoll API mainly consists of epoll_create1, epoll_ctl, and epoll_wait. We have basic shims for all these functions but currently our epoll support is mostly a stub, since the actual polling part is still missing. (Also the behavior of
dup
on an epoll file descriptor is likely wrong.)Implementing this is non-trivial, since it introduces a new kind of blocking to Miri: block until any of a set of FDs is read for reads/writes. We currently don't have any notion of file descriptors blocking at all, so this will need some careful design We probably need some notion of a per-file-descriptor wait lists of threads that are blocked on this FD? We should probably have eventfd and socketpair implemented first so that we have some examples of blocking FDs to consider.
Also note some interesting tidbits in this SO question: we may have to explicitly implement the concept of a file description as that seems to be observable through the epoll APIs. On the plus side this means we can implement
dup
once and for all and we don't have to rely on each and every FD type doing it correctly.The text was updated successfully, but these errors were encountered: