-
Notifications
You must be signed in to change notification settings - Fork 404
Description
Our socketpair and eventfd implementations currently do not support blocking.
To fix that will require a bit of re-structuring to enable FileDescription::{read,write} to block. In that case we can't use the convenient bytes: &mut [u8]/bytes: &[u8] arguments, we need the underlying Miri place, so that we can store it in a callback to be used on unblocking. (Incidentally that would also simplify eventfd read/write a bit since we could use the normal memory APIs to reading/writing u64 in an endianess-aware way, rather than having to implement that on a byte slice.) The functions also need access to the return place so they can write the return value later, when they are unblocked.
Basically, a bunch of the convenience that is currently implemented here can't be used when blocking is involved. We have to make read/write lower-level functions that look more like the usual Miri hooks, and possibly add some helper functions to make it still easy to implement the current behavior. (Those helper functions are then likely useful with other file system functions as well.)