Comment by topspin
7 months ago
It's tragic, and it bothers me that Jens Axboe's work is suffering due to this. Obviously, with the clarity of hindsight, this might have been avoided. Now the cost of the damage it high.
My idea: consider formal verification. A rigorous formal proof of behavior is capable of solving actual flaws and probably capable of overcoming the bad PR.
That would require a great and ongoing effort. However, given the nature of io_uring, it's likely rather amenable to formal verification, and ultimately it is probably necessary. Perhaps our new "AI" tools could greatly reduce the effort.
Anyhow, that's my brilliant thought...
Replying to myself.
io_uring is only a more ambitious manifestation of a pattern that has been commonplace for a long time. High performance network, storage and other hardware use circular buffers internally in their drivers to process commands and return results. io_uring is attempting to realize the same pattern, but for the entire operating system interface.
That's a really big idea. It has me asking whether this isn't how all "IPC" should be done, where one generalizes all of the running processes, including the "kernel." Ultimately it has significant implications for CPU architecture, supplanting traditional patterns.
When I wrote "given the nature of io_uring," I had something specific in mind wrt formal verification. io_uring fundamentally consumes a stream of bytes. At the front end of that is a great deal of validation code to ensure the steam contents are sane. At the backend, the commands are mapped to existing kernel functionality. It's the front end I think could be well served by formal verification.