Open RalfJung opened 2 weeks ago
Alternatively we could implement it similar to sleep
, but instead of waking on the next instruction, just reexecute the current one.
That does mean we cannot mutate any state before blocking or we'd get incorrect behavior
sleep
uses the same blocking machinery as everything else. We don't currently use the "re-execute instruction" approach for anything and TBH I think that is a bit too hacky for my taste. For instance if an intrinsic argument is *ptr
then we don't want to re-load it from memory each time... though I guess if the value would change that would be a data race so it doesn't actually make a difference?
May I work on this issue? Or it belongs to a larger project? I don't want to block others' work :-)
I think my work on #3448 might potentially block this. The current specification for epoll is only for non-blocking eventfd and socketpair. I wish to let that land then incorporate blocking mechanism to it.
I see. Thanks for letting me know. I'll look for something else then.
Our
socketpair
andeventfd
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 convenientbytes: &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.)