diff --git a/Hardware/index.md b/Hardware/index.md index 9b0053dc64..7ac52847e8 100644 --- a/Hardware/index.md +++ b/Hardware/index.md @@ -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 diff --git a/projects/sel4/kernel-contribution.md b/projects/sel4/kernel-contribution.md index b088b1d750..4e958bfb02 100644 --- a/projects/sel4/kernel-contribution.md +++ b/projects/sel4/kernel-contribution.md @@ -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 @@ -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. @@ -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 @@ -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 @@ -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. diff --git a/projects/sel4/platf-owner.md b/projects/sel4/platf-owner.md new file mode 100644 index 0000000000..1eb9f90783 --- /dev/null +++ b/projects/sel4/platf-owner.md @@ -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.