Re-work section on porting seL4 to new platforms

Signed-off-by: Ivan Velickovic <[email protected]>

projects/sel4/porting.md

@@ -7,53 +7,109 @@ SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
 
 # Porting seL4 to a new platform
 
+This section covers porting a new ARM or RISC-V platform to seL4. You can check the list of supported seL4 platforms [here](https://docs.sel4.systems/Hardware/).
+
 ## Setup
 
 In order to load the seL4 image (via some means) it is important to have a working bootloader.
-We tend to use [U-boot](https://www.denx.de/wiki/U-Boot) as it is open source, reliable and supports many different architectures.
+We tend to use [U-Boot](https://www.denx.de/wiki/U-Boot) as it is open source, reliable and supports many different architectures.
+
+There are a variety of ways of loading an seL4 image from U-Boot such as eMMC, TFTP, and USB.
 
-For initial setup you can follow the instructions on the UNSW advanced operating systems website regarding [setting up a tftp server](https://www.cse.unsw.edu.au/~cs9242/19/project/linux.shtml).
+For setting up a TFTP server to transfer images over the network, you can follow the
+[UNSW Advanced Operating Systems course guide](https://www.cse.unsw.edu.au/~cs9242/19/project/linux.shtml).
 
-Once you get U-boot up and running it is a good idea (if the platform is supported) to flash a
-Linux image onto the dev board. This way you can find the correct address to load the image into memory.
+Once you get U-Boot up and running it is a good idea (if the platform is supported) to flash a
+Linux image onto the board. This way you can find the correct address to load the image into memory.
 This is also useful for debugging, as you can use the FDT file system to dump addresses from a running system.
 
 Once you have found the correct address to load, you can use the command `bootcmd="tftpboot 0x20000000 sel4_image && go 0x20000000"`
-(using 0x20000000 as an example) followed by `saveenv` to save the starting address onto the boards flash memory.
-You will also need to set the 'ipaddr' and 'serverip' details can be found in the link above.
+(using `0x20000000` as an example) followed by the `saveenv` command to save the starting address onto the boards flash memory.
+
+You will also need to set the `ipaddr` and `serverip` environment variables, details can be found in the link above.
 
 ## seL4
 
-In order to have a successful port of seL4 to your target ARM platform you will need to go through the following steps.
+In order to have a successful port of seL4 to your target ARM or RISC-V platform you will need to go through the following steps.
+
+### Device Tree
+
+Device Trees are used by ARM and RISC-V platforms to describe the hardware platform,
+seL4 makes use of Device Trees at build time which is why acquiring a Device Tree Source (DTS)
+for your platform is one of the first steps.
+
+seL4 relies on the DTS for the location and size of main memory as well as information
+about certain devices used by the kernel such as the timer. In debug mode, seL4 also
+makes use of the default serial device for debug output.
 
-### DTS
+Typically the Device Tree Source will be included in the
+[Linux kernel source](https://github.com/torvalds/linux), from there you can decompile
+the device tree blob (DTB) from building the Linux kernel to get device tree that
+Linux uses.
 
-Look for DTS and drivers inside the [Linux repository](https://github.com/torvalds/linux), normally they will be supported. If they are supported clone Linux and modify the `update-dts.sh` to add your target. Run the script located in `kernel/tools/dts/update-dts.sh` at the cloned Linux repository. This will create a "platform.dts" file from Linux inside the dts folder in the kernel. You may need to add device nodes depending on what Linux uses and what is required by seL4. For example, in the port of the Rockpro64 a memory node and an extra timer node were needed so these had to be defined manually.
+You can compile the Linux Device Tree Sources into a final Device Tree Blob with:
+```sh
+make ARCH=<arm/arm64/riscv> CROSS_COMPILE=<TOOLCHAIN> defconfig
+make ARCH=<arm/arm64/riscv> CROSS_COMPILE=<TOOLCHAIN> dtbs
+```
+
+The DTBs can be found in `arch/<ARCH>/boots/dts/`.
+
+The following command allows you to decompile the DTB:
+```sh
+dtc -I dtb -O dts /path/to/dtb > linux.dts
+```
+
+It should be noted that you may need to add device nodes depending on what Linux uses
+and what is required by seL4. For example, in the port of the ROCKPro64 a memory node
+and an extra timer node were needed so these had to be defined manually.
 
 ### Hardware generation script
 
-Depending on your platform and the way the DTS is defined you may need to modify the hardware_gen.py script.
-From the above example the Rockpro64 needed a memory node so that this script could define working memory.
+Depending on your platform and the way the DTS is defined you may need to modify the `hardware_gen.py` script.
+
+From the above example the ROCKPro64 needed a memory node so that this script could define working memory.
 Other gotchas could include interrupt cells, interrupt numbers being mapped wrongly, or incorrect addresses.
 Also serial and timer drivers will need to be added to the kernel if they don't already exist. You can check this through
-the DTS device strings and compare to the hardware.yml file in `kernel/tools/hardware.yml`. If needed add the required drivers in `kernel/drivers/`.
+the DTS device strings and compare to the hardware.yml file in `seL4/tools/hardware.yml`.
+If needed, add the required drivers in `kernel/drivers/`.
 
 ### Kernel
 
-You will need to add `libsel4/sel4_plat_include/<platform>/sel4/plat/api/constants.h` and add sel4_UserTop depending on what you support. Look in the other platform files for examples similar to your platform.
-
-### CMake-build system
+You will need to add `seL4/libsel4/sel4_plat_include/<platform>/sel4/plat/api/constants.h`,
+depending on your platform, this is either empty or requires defining the value for `seL4_UserTop`.
+Look in the other platform files for examples similar to your platform.
 
-You will need to modify the build system in two places. Firstly in the kernel's platform folder, you define `kernel/src/plat/<platform>/config.cmake`, again you can look at other platforms for examples.
-Secondly, you will need to add 'KernelPlatform' to the cmake and elf-loader tools. You can do this by editing
-`tools/cmake-tool/helpers/application_settings.cmake` and `tools/elfloader-tool/CMakeLists.txt`.
+You will need to add a CMake configuration file for the platform at `kernel/src/plat/<platform>/config.cmake`.
+It is best to base the contents of this file off of other platforms of the same architecture.
 
 ### ELF-loader
 
-You will need to add directories and files `tools/elfloader-tool/src/plat/<platform>/sys_fputc.c` and
-`tools/elfloader-tool/include/plat/<platform>/platform.h` which will provide a simple implementation of putchar with a physical address for uart for the elf loader to use.
+Although we use U-Boot as a bootloader, there are additional steps needed to initialise the
+hardware and setup system images before we can boot seL4. This is the purpose of the
+[ELF-loader](https://docs.sel4.systems/projects/elfloader/).
 
-## seL4 test
+The code for the ELF-loader can be found in the `elfloader-tool` directory at the root of
+the [seL4_tools](https://github.com/seL4/seL4_tools) repository.
+
+Depending on your platform, you may have to make changes to the ELF-loader which is
+responsible for loading the kernel and any user-programs. The ELF-loader outputs to the
+serial, so needs to be able to access the UART.
+
+On RISC-V, outputting to UART is done via a call to the SBI layer so no changes are necessary.
+
+On ARM, there are a variety of existing UART drivers in `tools/elfloader-tool/src/drivers/uart/`,
+if the default serial is not supported by any of these drivers, you will have to
+provide a simple putchar implementation.
+
+If the ELF-loader needs to be a particular file format (e.g binary or EFI) or needs to start at a
+particular physical address, you can configure the default platform options in
+`seL4_tools/cmake-tool/helpers/application_settings.cmake`.
+
+## Testing your seL4 port
+
+In order to sanity check your port of seL4, it is a good idea to get
+[the seL4test project](https://docs.sel4.systems/projects/sel4test/) running and passing.
 
 seL4test needs user level serial and timer drivers to run. Add these drivers and the following files to libplatsupport in
 order to get the test suite running. The directory structure and files will look something like the following. Some of these
@@ -62,24 +118,38 @@ files may not have anything in them but include them anyway to keep the build sy
 Use the other platforms as examples; generally you will have to configure the timer driver by reading the manual, it may have its
 own unique programming sequence and can sometimes be a bit tricky.
 
+If the technical reference manual does not contain enough detail, you may be able to gain more information by looking at the
+respective Linux driver for the device. This can be done by searching for the value of the 'compatible' field that is on
+each device node in a DTS in the Linux source code.
+
 You can find the physical addresses and interrupt numbers for each device in its platform reference manual and copy them into the right places.
 
-`libplatsupport/plat_include/<platform>/`
-	-`clock.h`
-	-`gpio.h`
-	-`i2c.h`
-	-`mux.h`
-	-`serial.h`
-	-`timer.h`
-`libplatsupport/src/plat/<platform>/`
-	-`chardev.c`
-	-`ltimer.c`
-	-`serial.c`
-	-`timer.c`
+`util_libs/libplatsupport/plat_include/<platform>/`
+* `clock.h`
+* `gpio.h`
+* `i2c.h`
+* `mux.h`
+* `serial.h`
+* `timer.h`
+
+`util_libs/libplatsupport/src/plat/<platform>/`
+* `chardev.c`
+* `ltimer.c`
+* `serial.c`
+* `timer.c`
+
+### sel4test configurations
+
+The default configuration of seL4 in sel4test is non-MCS, single-core, with no hypervisor mode. After confirming that the default
+configuration successfully runs, it is a good idea to test the more complex configurations with your port as well.
 
 ### Gotchas
 
 Incorrect address alignment and incorrect memory regions can cause instruction faults. One way to debug this, is
 to shorten memory regions in DTS memory nodes to check you are touching the correct area.
 
-Once you have succeeded with your port and have seL4 test passing in release mode, you can add an entry to the CHANGES file describing the platform you added and submit a pull request on the seL4 github.
+## Contributing
+
+Once you have succeeded with your port and have seL4 test passing in release mode, you can add an entry to the CHANGES file
+describing the platform you added and submit a pull request on the [seL4 GitHub](https://github.com/seL4/seL4.git) as well
+as any other repositories changes such as [util_libs](https://github.com/seL4/util_libs.git).