Skip to content

Commit

Permalink
hardware: info for not supported platforms (#230)
Browse files Browse the repository at this point in the history
* supported platforms page:
  * added a "Not in the lists below?" section

* kernel-contribution.html:
  * added an intro paragraph linking back to the supported platforms
    page and other options than developing yourself
  * Added link to new platform owner page
  * BSD -> BSD/platform (the porting page uses 'platform')
  * fixed small typo (Contrbution)

* new platform owner page


Signed-off-by: June Andronick <[email protected]>
Co-authored-by: Gerwin Klein <[email protected]>
  • Loading branch information
june-andronick and lsf37 authored Mar 15, 2024
1 parent 41503b0 commit 983ea6e
Show file tree
Hide file tree
Showing 3 changed files with 97 additions and 10 deletions.
31 changes: 31 additions & 0 deletions Hardware/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,37 @@ The seL4 proofs only hold for specific configurations, as noted in the *Verifica

More information can be found on the [Verified Configurations](../projects/sel4/verified-configurations.md) page.

### Not in the lists below?

If the platform, architecture, feature that you are after is not listed on this page,
you have several options, listed below. It is important to note however that, as
explained in the guidelines linked below, contributing new ports or features will require
compelling arguments, discussion with the technical community (including through
Request-For-Comments), as well as testing requirements and maintenance/expertise
commitment, to a degree depending on the nature of the contribution.


* You can contact one of the seL4 Foundation [Endorsed Services
Providers](https://sel4.systems/Foundation/Services/) to get commercial
support or professional advice to develop such a port or feature (with the
implications and expectations detailed in our [guidelines for contributing
kernel code](../projects/sel4/kernel-contribution.html));

* You can check the [roadmap](../projects/roadmap.html) for any planned
contributions, from the seL4 Foundation or larger community, such on any new
architecture ports, new large formal verifications, or large or fundamental
new features;

* You can contact the seL4 community through one of our [communication
channels](https://sel4.systems/contact/) to ask whether someone is developing
such a port or feature already, or whether there is general interest in discussing
such a new port or feature;

* If you are in a position to develop the seL4 port or feature yourself, you
should follow our [guidelines for contributing kernel
code](../projects/sel4/kernel-contribution.html), which details the
implications and expectations.


### Simulating seL4

Expand Down
29 changes: 19 additions & 10 deletions projects/sel4/kernel-contribution.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,14 @@ SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.

# Contributing to kernel code

If the platform, architecture, feature that you are after is not listed on the
[Supported Platforms page](/Hardware/), and if, from your available
[options](/Hardware/index.html#not-in-the-lists-below), you choose to contribute
the port or feature yourself, here are the guidelines for it.

There four classes of kernel contributions possible:

1. Board Support Package (BSP) ports
1. Board Support Package (BSP) ports, also known as platform ports.
2. Architecture features
3. Architecture ports
4. Kernel features
Expand All @@ -18,13 +23,17 @@ benefit from the seL4 proofs), until the proofs themselves are also
appropriately modified, or it can be shown that the modifications do not
affect the proofs.

## BSP ports
## Platform/BSP ports

*Platform ports*, also known as *Board Support Package (BSP) ports* are the
simplest, and require the least modifications, discussion and approval. This
assumes that you are porting the kernel to a new board on an existing
architecture.

*BSP ports* are the simplest, and require the least modifications, discussion
and approval. This assumes that you are porting the kernel to a new board on
an existing architecture.
The main thing is to:

The main thing is to follow the [BSP Porting guide](/projects/sel4/porting).
* follow the [platform porting guide](/projects/sel4/porting);
* follow the guidelines to [become a platform owner](/projects/seL4/platf-owner.html).

Questions, discussion, and sharing of work in progress during this stage are
welcome.
Expand All @@ -44,7 +53,7 @@ Once the code is ready for submission follow the

## Architecture features

In some cases a kernel port requires more than just a BSP port. If the port is
In some cases a kernel port requires more than just a platform/BSP port. If the port is
on a supported architecture, but you wish to make use of architecture features
that the kernel does not yet support, then these will be *architecture feature
contributions*. This will typically require moderate modifications to kernel
Expand Down Expand Up @@ -86,12 +95,12 @@ code that does affect the verified part of the kernel.
Consider whether you want to have the architecture feature
implementation verified, and the plans for achieving that.

As with a BSP port make sure to write appropriate tests and include
As with a platform/BSP port make sure to write appropriate tests and include
them in seL4test as part of the work. Consider (and discuss) a plan
for how to support this port (e.g. with regression testing) so that it
continues to be updated and work as seL4 evolves.

Once the implementation is complete follow the [Contrbution
Once the implementation is complete follow the [Contribution
Guidelines](processes/contributing.html) for submitting changes.

## Architecture Ports
Expand Down Expand Up @@ -133,7 +142,7 @@ re-implement to avoid them.
Consider whether you want to have the port verified, and the plans for
achieving that. Verifying an architecture port is a significant undertaking.

As with a BSP port, make sure to write appropriate tests and include
As with a platform/BSP port, make sure to write appropriate tests and include
them in seL4test as part of the port. Consider (and discuss) a plan
for how to support this port (e.g. with regression testing) so that it
continues to be updated and work as seL4 evolves.
Expand Down
47 changes: 47 additions & 0 deletions projects/sel4/platf-owner.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
---
SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
---

# Becoming a platform owner

Below are the guidelines defined by the [Technical Steering Committee
(TSC)](https://sel4.systems/Foundation/TSC/) to become a *platform owner*.

This assumes that:
* the platform that you are after is not listed on the [Supported Platforms
page](/Hardware/);
* from your available [options](/Hardware/index.html#not-in-the-lists-below),
you choose to contribute the port or feature yourself;
* you are following the [guidelines for kernel
contributions](/projects/sel4/kernel-contribution.html#) and the specific
[Platform Porting guide](/projects/sel4/porting).

> 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.

0 comments on commit 983ea6e

Please sign in to comment.