On 31 Jul 2021, at 17:35, Andrew Warkentin
The patches are only for the boot code at the moment, which isn't part of the verification. However, I may end up having to fork seL4 at some point
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/).
because the seL4 project's priorities seem to be heavily focused on static deeply embedded systems rather than desktops, servers, and large embedded systems.
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... Gernot