Docsite content: hardware: instructions if board not in the list

[june-andronick]

On https://docs.sel4.systems/Hardware/ we want to have instructions on what to do if the board you want is not in the list.

[june-andronick]

We have this porting page.

Questions:

• are the instructions on this page up to date? If not, who has the knowledge to update them?

• the instructions on this page say they are for ARM platforms; do we have instructions for RISC-V and x86?

• is this page what we aimed for when wanting instructions on "what do to do if the board you want is not on the supported hardware list"? Do we just want a pointer to it (once updated if needed)? Or do we want more than instructions on how to do it, e.g. how to have it tested, reviewed, accepted by the Foundation, listed under the supported platforms etc?

@lsf37 @Indanz @Ivan-Velickovic @gernotheiser @wom-bat opinions?

[Ivan-Velickovic]

are the instructions on this page up to date? If not, who has the knowledge to update them?

No, I did start making the page up to date a while ago. I can't find the changes right now but I'll have a look when I get back from leave in a week and make a PR.

the instructions on this page say they are for ARM platforms; do we have instructions for RISC-V and x86?

I can add instructions for RISC-V but I don't have enough knowledge for x86. Someone else would probably have to do that part.

is this page what we aimed for when wanting instructions on "what do to do if the board you want is not on the supported hardware list"? Do we just want a pointer to it (once updated if needed)? Or do we want more than instructions on how to do it, e.g. how to have it tested, reviewed, accepted by the Foundation, listed under the supported platforms etc?

I think the porting page should also contain what is necessary to have it accepted by the Foundation. Right now it isn't clear to me if porting just the kernel is sufficient or if contributing platform support should also contain changes for sel4test etc. This becomes more complicated now with seL4 Microkit as well.

I guess it's not fair to expect contributors to add support to projects that they don't plan to use (e.g sel4test or Microkit) but at the same time that will make the eco-system more fragmented.

[lsf37]

I think the porting page should also contain what is necessary to have it accepted by the Foundation. Right now it isn't clear to me if porting just the kernel is sufficient or if contributing platform support should also contain changes for sel4test etc. This becomes more complicated now with seL4 Microkit as well.

I guess it's not fair to expect contributors to add support to projects that they don't plan to use (e.g sel4test or Microkit) but at the same time that will make the eco-system more fragmented.

The TSC discussed this back in Feb 2021 and reached he following conclusion:

A platform owner:

• is the maintainer of platform specific kernel and library code for that platform

• is the “driver” for that platform (setting the direction where things are going for the platform)

• is usually one of the main code contributors for that platform

• has the following responsibilities:

  • keep the platform working, make sure sel4test and sel4bench are passing on the
    master branch for all supported configurations (esp MCS, but also multicore, and
    IOMMU/VCPU where relevant/appropriate)

• write and maintain documentation for the platform,

• help to keep the verification passing for verified configurations (only relevant for a
  few platforms, but might increase in the future)

• handle bug reports for that platform on github and devel mailing list
  (has access to github issues and/or the new sel4 Jira at sel4.atlassian.net for
  this if desired)

• handle support requests/questions for that platform (if low-key, ideally publicly on the
  mailing list, but also paid support etc for bigger things)

• review and help merge PRs for that platform (relevant PRs should have
  one approving review from the platform owner if possible)

• providing binaries for bootloader and load instructions would be desirable

• if other development on the master branch has platform impact (from contributions or D61),
  it should preferably include relevant platform code updates already, but might need consultation
  with the platform owner to get done, i.e. the basic expectation would be “you break it,
  you fix it”, but people sometimes might need help.

• the foundation advertises platform owners on the website, and platform
  owners would link back to the foundation.

Note that this was back in D61 times still and could be revisited. In general, the goal is not to receive as many platform ports as possible. Each new port adds maintenance work for a very small set of people. The only way this can scale is if the set of people who maintain code increases with the set of contributions.

"Platform owner" is not quite the same as criteria for accepting a platform port, but we should minimise accepting unmaintained ports, so either we maintain ourselves and have the necessary hardware, or there needs to be an owner for a new port that comes in.

The absolute minimum for a new port should be that it passes sel4test and sel4bench, otherwise it's not even clear which features are there. Adding further things like CAmkES, VMs, microkit, etc could (maybe should) be optional, but from the perspective of people wanting to use a port, it's very annoying if we have a big table of supported platforms when then most of the infrastructure then doesn't work for it.

[Ivan-Velickovic]

The TSC discussed this back in Feb 2021 and reached he following conclusion:

Ah okay I did not realise it was something the TSC has already discussed. I couldn't find this information myself so I think whatever the TSC decides on should be either linked to from the porting page or on the porting page itself.

[lsf37]

The TSC discussed this back in Feb 2021 and reached he following conclusion:

Ah okay I did not realise it was something the TSC has already discussed. I couldn't find this information myself so I think whatever the TSC decides on should be either linked to from the porting page or on the porting page itself.

Agreed, I should definitely put this somewhere more public.

[Indanz]

is this page what we aimed for when wanting instructions on "what do to do if the board you want is not on the supported hardware list"?

No, I don't think so. Porting it yourself is only one of the options. And there are also different kind of porting: Porting to a new architecture, porting to a new CPU, porting to a new board with existing SoC, porting to a new SoC.

First thing should be to see if an already supported platform uses the same SoC and if so, adjust for the changes with an external DTS file.

Do we just want a pointer to it (once updated if needed)?

I think so yes.

Or do we want more than instructions on how to do it, e.g. how to have it tested, reviewed, accepted by the Foundation, listed under the supported platforms etc?

That too, but it should be on the porting page.

the instructions on this page say they are for ARM platforms; do we have instructions for RISC-V and x86?

ARM and RISC-V don't have a standardised system platform like x86 has. For those it's pretty much necessary to compile per platform.

x86 historically never needed a binary per platform, all differences are runtime discoverable, from PCI devices to CPU features. So there is no need to "port" from one x86 platform to another, they should all be pretty compatible.

That said, there are vendor and CPU generation specific features for e.g. virtualisation and IOMMU which currently only have some Intel support and nothing for AMD. So porting on x86 means adding support for newer features, which then can be used on all platforms having those features, while porting on ARM/RISC-V usually implies adding support for a specific platform.

Because of this, unlike ARM/RISC-V, where people expect to need to put some effort in before being able to use seL4, x86 users just expect things to work and aren't as quickly inclined to put the effort into making their use case work themselves.

In general, the goal is not to receive as many platform ports as possible. Each new port adds maintenance work for a very small set of people. The only way this can scale is if the set of people who maintain code increases with the set of contributions.

I disagree strongly with this. If you want people to use seL4 more widely, you need as many platforms as possible. Also, the more platforms are supported, the more cpu versions and uart/timer drivers will be implemented, reducing the effort for future ports. That said, I don't think it's necessary to actively support hardware that's not for sale any more.

For AArch64 for instance, a platform port isn't that much work, except if it uses a yet unsupported CPU or interrupt controller. For user space it's pretty much limited to adding timer and UART drivers. However, because the build system does things per platform, it's not easy to just configure a user's board and build for that, it needs to be added explicitly.

To me it would make more sense if seL4 had generic support for different cpu types etc. and had example configurations for specific boards. That's more or less what we have now, but AFAIK there's no way for a user to build seL4 without selecting a platform specifically and setting the variables normally set in config.cmake.

For ARM and RISC-V it would make much more sense to do things per range of SoCs, instead of per board.

keep the platform working, make sure sel4test and sel4bench are passing on the
master branch for all supported configurations (esp MCS, but also multicore, and
IOMMU/VCPU where relevant/appropriate)

But all those configurations are almost platform independent. The only addition MCS has is that the timer needs to be reconfigurable, so it might stress the timer driver more and flush out bugs there (but modern hardware has standardised system timers). The hardware specific part of multicore support is mostly the cache synchronisation instructions, but otherwise it should also be platform independent. IOMMU and VCPU need specific hardware support, but those are, like multicore, architecture dependent, not platform dependent.

seL4 currently misses a low level hardware test which tests whether all the low-level hardware functionality does what the seL4 kernel assumes it does. If we had that, testing whether a specific platform works could be much quicker. Easier said than done to implement this though, bugs can be subtle or timing sensitive and some features may just be impossible to test.

Adding further things like CAmkES, VMs, microkit, etc could (maybe should) be optional, but from the perspective of people wanting to use a port, it's very annoying if we have a big table of supported platforms when then most of the infrastructure then doesn't work for it.

Infrastructure should be independent from ports. Other than missing timer and UART drivers, which are easily copied from sel4test/sel4bench, what's needed for basic support for CAmkES, VMs, microkit? Users probably have to update the DTS file for their usage anyway.

I think the requirements for a new platform should depend on how much it differs from already supported ones. If the changes are limited to src/plat/ and a UART driver, the bar should be very low (sel4test and sel4bench passing). The more changes or new hardware types added, the higher the bar. For new hardware the Foundation should get a board for the CI system.

The TSC list of requirements sounds like something that should be required for things like Morello support. But if you want people to contribute ports at all, the bar shouldn't be that high for most ports.

[june-andronick]

Thanks @Ivan-Velickovic @Indanz and @lsf37 for your comments.

Trying to summarise (feel free to comment): we should have a porting page, linked from the hardware page, that has:

• options available: getting help from service providers, contacting the Foundation, doing it yourself (with instructions included)
• for doing it yourself:
  • we should have up-to-date instructions for platform ports for Arm and RISC-V (but not x86)
  • we should have expectations (to be refined when I write the draft):
    • minimal tests to pass
    • commitment to be a maintainer (with definition) or acceptance to be maintained by Foundation (with requirements for that)
    • provide all the info we need for the table in the supported platform list?

@Ivan-Velickovic when do you think you will be able to have that done? Do you think you could have it done in the next 3-4 weeks? Let us know if you need help. Once it's done I'll work on drafting the extra info above aiming to have it all done by mid March to fit in the project.

@Indanz you raise a number of other points, which I don't know enough about to comment on. Waiting on @lsf37 to comment :)

[Ivan-Velickovic]

@Ivan-Velickovic when do you think you will be able to have that done?

I'll do it tomorrow, thanks for reminding me.

[june-andronick]

@Ivan-Velickovic when do you think you will be able to have that done?

I'll do it tomorrow, thanks for reminding me.

@Ivan-Velickovic this seems to still be open. Would you be able to have it updated as soon as you can (for Arm and RISC-V)? It is part of the NCSC deliverable. Thanks!

[june-andronick]

Other than that, the rest should now be done in this PR: seL4/docs#230

I've re-used the kernel contribution code, which was very detailed but not in any sub-menu and only linked (AFAICT) from the Tutorial's page.