-
Notifications
You must be signed in to change notification settings - Fork 394
Description
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.