On 7/31/21, Gernot Heiser
While we cannot prevent forking (but strongly discourage it), please note that you cannot use the name seL4 for an incompatible fork (with a research exception for “experimental” versions, see https://sel4.systems/Foundation/Trademark/).
I'm well aware of that. If I do end up forking I would rename my fork. Since there will be no raw API access or multi-personality support, seL4 will really just be an implementation detail as far as everything outside the process server and base system library will be concerned.
seL4’s notion of priorities are microkernel-style: simple mechanisms that are as policy-free as possible. Actual policies (like the Linux CFS) can (and should) easily be implemented at user mode. See Lyons et al [2018] which implemented EDF scheduling at user level: https://trustworthy.systems/publications/csiroabstracts/Lyons_MAH_18.abstrac...
I don't really want to add stuff to the kernel unless I absolutely have no other options. I can think of at least a few relatively simple features I want that probably wouldn't get accepted. One is a system call origin limit to allow trapping foreign system calls for things like Linux binary compatibility. I'd mentioned this earlier and someone said something like that could be done with virtualization, but it is completely unacceptable to require that hardware virtualization be enabled just to run Linux binaries, not to mention the requirement for a server to intercept every system call (foreign or native) in such an environment, whereas an origin limit would allow for a purely library-based compatibility layer that can replace traps with function calls as they occur. Another I can think of is a hook for a per-core thread that automatically migrates a thread from another core when the original assigned core is running another thread but another core is free. I can't think of any way to do it well without a hook in the kernel to run a core's migration thread only when that core is idle, since the migration thread would always have to be runnable. Is there any way automatic migration can be done without such a hook and without the migration thread having to sleep? Also, if cross-core IPC gets removed that would pose a problem since UX/RT will have a uniform Unix-superset IPC model (with extra read/write-type functions that expose registers and a shared buffer) that needs to work between arbitrary threads regardless of if they are on different cores. Support for passive threads will be exposed to user programs, but I definitely don't want to require that one thread in every IPC exchange must be passive.