On 8 Mar 2025, at 22:02, Andrew Warkentin via Devel <devel@sel4.systems> wrote:
On Sat, Mar 8, 2025 at 3:12 AM Gernot Heiser via Devel <devel@sel4.systems> wrote:
I don’t see a reason for providing bulk data copying as a kernel service (despite Liedtke doing this in the original L4, in violation of his own minimality principle). It can (and therefore should) be provided as a user-level service, which is why we dropped it in seL4. And, done properly, it’ll easily outperform QNX’s in-kernel implementation.
I can't come up with a way for such a service to determine the server's address space short of tying endpoints to server address spaces, which is something I want to avoid, since I want the option of handing off connections to threads/processes with different address spaces. The other issue is with mapping the source and destination address spaces; the most "straightforward" ways I can think of to do this would either be to map both source and destination buffers on every IPC, which would be extremely inefficient (especially with the requirement to have a separate capability for each VSpace a page or table is mapped into, meaning one system call would become potentially hundreds or more depending on the buffer sizes), or have an identity mapping of all of physical memory with user-level shadow page tables to look up each page before copying it, which could also be somewhat slower than what could be done in the kernel, where you could have table-sized address space windows reserved for source and destination address spaces, with only two table updates required if both buffers lie within a single table's address space. I did actually end up using the kernel's physical address space window and software walking of page tables in my initial in-kernel implementation since it might have ended up being slightly easier to do initially, but at some point I want to replace it with a table-window-based setup.
Why so complicated? The equivalence of putting the functionality in the kernel, where the kernel has access to all user state, is to have a trusted server which has access to all client state (especially CSpaces). The TCB is the same, but you don’t break verification and retain the option to verify the trusted server. This approach will work for all designs. In a specific system design you’re likely have opportunities to simplify/modularise/reduce the power of the server, making verification easier. But even the model of the all-powerful server is better (more assured) than the model of hacking the kernel and completely abandoning verification. Gernot