On 7/31/21, William ML Leslie <william.leslie....@gmail.com> wrote: > On Sat, 31 Jul 2021, 8:54 pm Andrew Warkentin, <andreww...@gmail.com> > wrote: > >> >> Even though the process server will run in user mode as far as the >> hardware and microkernel are concerned, functionally it will be akin >> to something above user processes but below the kernel. It will have >> full access to all kernel objects in the system including all user >> pages, CNodes, and endpoints (it won't actually map user pages except >> if a process opens the associated file for read/write I/O as opposed >> to mapping the file), > > > Eeep. You want untyped access to cappages? >
The process server won't have any kind of raw access to the underlying memory of kernel objects like CNodes, since the API doesn't allow it. The only reason I can think of for adding support for anything like that might be to somehow allow raw read access (but certainly not write access) to make CSpace allocators more space-efficient by eliminating the bitmap used to track which slots are used, but that certainly isn't any kind of priority. > > I do understand that urge (for performance reasons). I would prefer to get > around that by implementing an io_uring style async interface to > kernel-implemented objects. The too-ing and fro-ing required to set up > address mapping is eventually going to get onerous and will have to be > solved with some rigour. > I've thought about that as well. I was thinking it could possibly be solved by adding a batch system call interface where the caller writes multiple system calls into a buffer (with each entry in this buffer having a fixed length including all registers, even ones that aren't used by a particular invocation) and passes the number of system calls to the kernel. This might best be implemented as an invocation on a new type of "batch buffer" kernel object rather than adding a new system call trap. _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
