guide_to_porting_sel4.md

Guide to Porting seL4

The level of work required and complexity of porting seL4 to a new platform is directly related to the level of similarity between the system to be ported and systems already supported by seL4. Porting seL4 to a new system based upon a SoC (system-on-chip) already supported by seL4 is likely to be relatively straightforward whilst porting seL4 to a system with a currently unsupported SoC is likely to require more work, e.g. requiring the addition of new serial and timer drivers.

As a starting point the user should read and understand the excellent guidance on porting supplied by the seL4 Foundation at this link.

The remainder of this section does not seek to repeat any information in the seL4 documentation; instead it provides more detailed guidance and worked examples based upon the experience of porting seL4 to the Avnet MaaXBoard.

Device Tree (DTS)

A device tree (DTS file) contains plain text data that describes a platform's hardware. A key requirement in porting seL4 to a new platform is the provision of a device tree describing the platform. A device tree can normally either be sourced from the Linux kernel or from a Linux distribution supplied by the platform manufacturer.

Device tree files are stored within the Linux kernel within the /arch/<arch_identifier>/boot/dts folders. For example, for ARM based devices DTS files may be retrieved from this link.

Support has not been incorporated into the mainline Linux kernel for the Avnet MaaXBoard, and therefore the device tree needed to be sourced from the platform-specific Linux distribution supplied by Avnet at this link.

Once a DTS file has been located it needs to be processed into a form suitable for inclusion in seL4, e.g. to remove use of C-style includes and macros. For the Avnet MaaXBoard this processing was performed using the following commands to generate DTS file named maaxboard.dts. It is expected the commands should be easily modifiable for other boards and sources of the Linux kernel. The following commands to be are executed within the build environment (i.e. the Docker container).

git clone https://github.com/Avnet/linux-imx.git
cd linux-imx
cpp -nostdinc -I include -I arch -undef -x assembler-with-cpp \
   arch/arm64/boot/dts/freescale/maaxboard-base.dts temp.dts
dtc -o temp.dtb temp.dts
dtc -o maaxboard.dts temp.dtb

Following creation of the platform's DTS file it should be stored in the /tools/dts folder of the seL4 git repository and the update-dts.sh script (located in the same location) updated to reference the new DTS file.

Previous Worked Examples

To help fully understand the guidance supplied by the seL4 documentation, it is informative to examine the changes made previously to the seL4 repositories to support new platforms. To that end the following links are to commits in the seL4 git repositories where support for platforms was added. It should be noted that to perform a basic port of seL4 to a new platform, i.e. sufficient to run and pass the seL4Test application, will require modification to the seL4, seL4_tools and util_libs git repositories.

• Avnet MaaXBoard - Port to platform with existing SoC support

  • seL4 commit
  • seL4_tools commit
  • util_libs commit

• ODroid C4 - Port to platform using an SoC very similar to previously supported SoC

  • seL4 commit
  • seL4_tools commit
  • util_libs commit

• Raspberry Pi 4 - Port to new SoC requiring new serial and timer drivers

  • seL4 commit
  • seL4_tools commit
  • util_libs commit

Testing the Port With seL4Test

To confirm the correct functionality of a port it is recommended that the seL4Test test suite is executed.

To build and execute seL4Test for testing purposes against forks of the seL4 git repositories the following procedure can be used. For the purposes of this example it is envisioned that the developer has forked the sel4, seL4_tools and util_libs git repositories under GitHub account work_account and performed the required modifications under branches named my_port. When following the instructions the commands will need to be modified to match the name of the developer's GitHub account and branch name.

1. Create a fork of the sel4test-manifest repository through the GitHub web interface and create branch my_port.

2. Modify file default.xml in the my_port branch of the forked sel4test-manifest repository to point at the developer's forks / branches. This will require the following changes.

   • Add a new remote to the manifest:

     <remote name="work_account" fetch="https://github.com/work_account"/>

   • For each modified repository update the associated project entry. For example, the entry for the seL4 repository would be changed from:

     <project name="seL4.git" path="kernel" revision="..." upstream="master" dest-branch="master"/>

     To the following:

     <project name="seL4.git" path="kernel" remote="work_account" revision="my_port" upstream="my_port" dest-branch="my_port"/>

3. Check out the newly updated manifest within the build environment:

   mkdir /host/seL4test
   cd /host/seL4test
   repo init -u https://github.com/work_account/sel4test-manifest.git -b my_port
   repo sync
   

4. Building and executing seL4Test can be performed by following the instructions previously provided in the Building Applications and Execution on Target Platform sections with the build commands modified appropriately to target the newly added platform.