[seL4] Re: Operating Systems built on top of seL4

On 7/31/21, William ML Leslie wrote:

On Sat, 31 Jul 2021, 8:54 pm Andrew Warkentin, 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.