hardware: info for not supported platforms (#230)

* 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]>

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
 

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.

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.