Pre-RFC: Supported kernel configurations

RFC discussion
1

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ā€.

Supporting Entities:

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.

Cost:

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.

Scope:

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.

Implementation:

Iā€™m not proposing any specific implementation at this point. It is important to first have a consensus that the proposed goals are appropriate.

1 Like
2

I think this could be clarified by having a clear set of support levels, similar to what is currently used by the Rust project to describe the extent of their support for different build targets: Platform Support - The rustc book

3

(Note: Testing commenting using ā€œMailing List Modeā€ - Not sure if this will work.)

I think using the Tier concept could work very well.

Ziglang also usies this system: https://ziglang.org/learn/overview/#tier-system

I think if there is agreement on ā€˜the problemā€™ then tierā€™s could be a great part of the solution.

4
  • There is a supported platforms page that lists various hardware platforms and has some great documentation on getting started on the listed platforms.

Thereā€™s also a seL4 kernel status page (Project Status | seL4 docs) that tries to capture what configuration options are available, their status and who is maintaining them. However this page doesnā€™t address many of the issues raised above.

5

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.

It also allows for lower verification costs as there is arguably a superlinear relationship between lines of code and verification effort.

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.

Also, as many of these config options arenā€™t mutually exclusive or independent and so any combination can provide a different kernel with different behavior. So the state space quickly is by far too large to exhaustively test.

It is anticipated that implementing this proposal would bring the following benefits:

I agree that with the listed benefits and agree that they are worthwhile.

Questions:

  • How standardized and specific should the supported definitions be? From a simple yes/no to an audit-able list of requirements that is tested regularly.
  • How centralized/decentralized should the support state be? A file in the repository that reflects supported status? This would mean that claiming to support a configuration by some entity would require endorsement by the project maintainers I think. Or can anyone claim that they support a configuration and there is only a convention that they respond to issues and requests.
  • What should happen when configurations are added and removed? Do new configurations need to have commitment to be supported before they can be added?
  • Will support requirements be transitive? If you support a specific configuration, will you need to transitively support that configuration in additional tools/libraries added in the future?