Re: [seL4] Benchmarks of seL4

On Tue, Apr 14, 2020, 12:17 AM Andrew Warkentin wrote:

On 4/13/20, Demi Obenour wrote:

...

Speaking of UX/RT: I strongly suggest avoiding PID-based APIs in favor of handle-based APIs, and allocating file descriptors in a way that is more efficient than always picking the lowest free one. The first causes many race conditions, and the second causes a lot of synchronization overhead. io_uring is also a good API to consider.

A Linux-like pidfd API will be present (although it will use procfs underneath; anonymous FDs will basically be absent from UX/RT). io_uring will probably be mostly implemented in the root system library, possibly with a few hooks in the root server.

On 4/13/20, Matthew Fernandez wrote:

...

This is effectively the approach CAmkES takes. Generated, specialised RPC entry points that use seL4’s IPC mechanisms. With enough information provided at compile time, you can generate type safe and performant marshaling code. With some care, you can generate code the compiler can easily see through and optimise. For passing bulk data, you can either

use

...

shared memory or unmap/remap pages during RPC.

When we did some optimisation work on CAmkES for a paper (~2014?) we were able to comfortably hit the limit of what one could have achieved with hand optimised IPC.

I'm planning to use static compile-time marshaling on top of a regular file descriptor for UX/RT's root server API. Since the only stable ABI will be that of the dynamically-linked root system library, the use of static marshaling shouldn't be a serious issue for binary compatibility. Most other subsystems using RPC will probably use dynamic marshaling.

Do you plan to support multikernel configurations and/or virtualization? How do you expect performance and security to compare to Linux? Sincerely, Demi