Below is a proposal that comes out of the postponed/abandoned RFC-6 proposal for seL4 core. This is not written in the RFC format as it is intended to be structured in a way to support discussion around the idea and motivation without making any specific proposal for an implementation.
Apart from the specific direct goals written below, the overall meta-goal here is to broaden the adoption of seL4 so that the impact created by the hard work of many people over many years is increased.
Proposal: As a system developer using the seL4 kernel it should be clear which build configurations are supported, and by whom they are supported.
Background / Assumptions / Current state / Definitions:
The kernel build system exposes a large number of options that can be set during a build. This is a good thing as it allows for experimentation and tuning of the kernel to specific use cases.
Individual kernel configuration options are well documented in the build system, however it is not necessarily clear which of these configurations work together or have been tested.
There is a supported platforms page that lists various hardware platforms and has some great documentation on getting started on the listed platforms.
There is not a clear definition of exactly what supported means.
A potential definition of supported could mean one or more of the following:
- The supporting entity has compiled the configuration and there are no compile errors.
- The supporting entity has incorporated the generated kernel.elf into some form of test system (possibly seL4), run this system on hardware, and all tests pass.
- The supporting entity believes that the specific configuration correctly implements the publish specification.
- The supporting entity has published a set of caveats / known bugs for the configuration.
- The supporting entity is willing to fix any bugs that are discovered (possibly as part of a paid support contract).
It is anticipated that implementing this proposal would bring the following benefits:
seL4 adopters / users have a better set of expectations going in to a new project
- this allows an adopter to select hardware that has support for the features they need
- this allows an adopter to better estimate any porting costs that may be involved in a new project
- this allows an adopter to understand where they can go for support
seL4 developers have users with appropriate expectations
- this allows for better triaging on reported problems
- this allows application of limited resources to be better applied
There is potentially scope for levels of support rather than simply supported and unsupported. For example perhaps there is benefit in marking a configuration as “we expect this works, but haven’t tried it ourselves and would welcome feedback and patches are definitely welcome” vs “we don’t expect this to work, it is not something we want to support, patches are not welcome”.
It is somewhat assume that the foundation would be the primary supporting entity. However, it may instead be a designated third party for some specific configuration.
Supporting a configuration takes resources and people, which places a cost on the supporting entity. It also practically limits the number of configurations that can be supported. The implementation plan should take this into account.
The scope of this proposal is intended to be only the kernel and libsel4 (which is currently bundled in the seL4 repo). It may be useful to apply this same proposal to other software components published by the seL4 foundation, however it would be useful to start with a narrow scope.
I’m not proposing any specific implementation at this point. It is important to first have a consensus that the proposed goals are appropriate.