On 2020-01-22 20:23, Heiser, Gernot (Data61, Kensington NSW) wrote:
Forking is a very bad idea. If you modify the kernel, you’re breaking verification, and it’s no longer seL4. And it will be one job of the Foundation to ensure that only things that *are* seL4 are called seL4.
Would you be willing to accept PRs that include the corresponding changes to the proofs, or which don’t affect verification? While I support and agree with your statement, I believe this fact is why so few people are using seL4 as a basis for new OS designs. If someone bases their operating system on seL4, they are limiting themselves to the features that can be implemented on top of seL4. I hope that it will someday be possible to implement any reasonable OS whatsoever on top of seL4, but I am not certain that is the case yet. And if someone finds that they need a feature (writing UEFI variables, 64-bit virtualization) that isn’t in seL4, they are stuck. They can’t implement the feature on top of seL4, and they can’t fork seL4 to implement it themselves. So they are facing a full rewrite. (UEFI variable support *must* be implemented in the kernel, because UEFI variables are accessed via privileged CPU instructions, not via MMIO or x86 I/O ports. Without it, it is impossible to modify the boot order on UEFI systems, which I consider to be an important feature.) Personally, I will consider seL4 to be feature complete when Linux could be ported to run as a user-mode process on top of seL4 without losing any features, and while still being scalable to thousands of CPUs. The choice of Linux is not important here. What is important is that seL4 is flexible enough to build any OS whatsoever on top of it, so that those building on top of it need not worry that it will get in their way. Does seL4 plan to be reach this feature set? While a “no” answer is obviously okay, I do think that the seL4 documentation should help OS writers determine if seL4 is a good base for them.
Gernot
Demi