Tutorial - lulu98/projects-with-sel4 GitHub Wiki

This tutorial gives a step-by-step guide on how to setup a proper development environment and get started with our seL4-/CAmkES-based OS framework.

QEMU is a system emulator that can emulate a full system, e.g. a Xilinx ZCU102 board. Using QEMU allows developers to develop without the need for physical hardware, while still being able to use real-world data for testing.

The Zynq 7000 ARM-based SoC family is one of the better supported QEMU emulation platforms. We use this QEMU emulation platform as a reference board to rapidly test our applications during development in case no hardware is available.

Build Instructions:

1. Adapt the following lines in .../src/build.sh script:

BUILD_APPS_PLATFORMS=(
    "hello-world zynq7000"
)

This tells the build system to build the hello-world application for the zynq7000 platform.

2. Build the application:

./build.sh

Execute instructions:

cd .../src/build_hello-world_zynq7000
./simulate

Expected Output:

1  ./simulate: qemu-system-arm -machine xilinx-zynq-a9  -nographic -serial null -serial mon:stdio -m size=1024M  -kernel images/capdl-loader-image-arm-zynq7000 
2  ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0
3    paddr=[564000..78c6bf]
4  No DTB passed in from boot loader.
5  Looking for DTB in CPIO archive...found at 67aee4.
6  Loaded DTB from 67aee4.
7     paddr=[3c000..3efff]
8  ELF-loading image 'kernel' to 0
9    paddr=[0..3bfff]
10   vaddr=[e0000000..e003bfff]
11   virt_entry=e0000000
12 ELF-loading image 'capdl-loader' to 3f000
13   paddr=[3f000..167fff]
14   vaddr=[10000..138fff]
15   virt_entry=187f8
16 Enabling MMU and paging
17 Bootstrapping kernel
18 Warning: Could not infer GIC interrupt target ID, assuming 0.
19 available phys memory regions: 1
20   [0..40000000]
21 reserved virt address space regions: 4
22   [e0000000..e003c000]
23   [e003c000..e003ee47]
24   [e003f000..e0168000]
25   [ff000000..ff100000]
26 Booting all finished, dropped to user space
27 Hello CAmkES World

Explanation to output:

• Line 1: The simulate script auto-generates a QEMU command as stated in this line. A short explanation: We use the ARM version of QEMU (qemu-system-arm) and specify to use the emulated machine Xilinx Zynq Platform Baseboard for Cortex-A9 (-machine xilinx-zynq-a9) and further instruct the guest to have 1GiB (-m size=1024M) of RAM. Furthermore, QEMU shall use the terminal window and output on the current console (-nographic -serial null -serial mon:stdio). The seL4/CAmkES kernel-/user-space binary images/capdl-loader-image-arm-zynq7000 is specified as the kernel image (-kernel images/capdl-loader-image-arm-zynq7000). For x86 platforms the kernel (passed with -kernel) and CapDL loader image (passed with -initrd) are separate binaries. For more information about QEMU, consult the official wiki or the man pages.
• Line 2-16: The elfloader is responsible for preparing the hardware for seL4 on ARM and RISC-V. It loads the kernel and user image (capdl loader) from an embedded CPIO archive, initialises secondary cores (if SMP is enabled), and sets up an initial set of page tables together with the MMU for the kernel.
• Line 17-26: seL4 microkernel initialization
• not shown: CapDL loader (root task = first user-space process/thread) output (can be turned on through compiler flag) -> sets up user space processes, e.g. our hello-world application
• Line 27: output of hello-world application

If you want to learn more about the seL4 microkernel, the CapDL loader and CAmkES, refer to the following pointers:

• seL4 documentation
• seL4 whitepaper
• CAmkES tutorial
• CapDL

Build Instructions:

1. Adapt the following lines in .../src/build.sh script:

BUILD_APPS_PLATFORMS=(
    "printer zynq7000"
)

This tells the build system to build the printer application for the zynq7000 platform.

2. Build the application:

./build.sh

Execute instructions:

cd .../src/build_printer_zynq7000
./simulate

Expected Output:

1  ./simulate: qemu-system-arm -machine xilinx-zynq-a9  -nographic -serial null -serial mon:stdio -m size=1024M  -kernel images/capdl-loader-image-arm-zynq7000 
2  ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0
3    paddr=[564000..78c6bf]
4  No DTB passed in from boot loader.
5  Looking for DTB in CPIO archive...found at 67aee4.
6  Loaded DTB from 67aee4.
7     paddr=[3c000..3efff]
8  ELF-loading image 'kernel' to 0
9    paddr=[0..3bfff]
10   vaddr=[e0000000..e003bfff]
11   virt_entry=e0000000
12 ELF-loading image 'capdl-loader' to 3f000
13   paddr=[3f000..167fff]
14   vaddr=[10000..138fff]
15   virt_entry=187f8
16 Enabling MMU and paging
17 Bootstrapping kernel
18 Warning: Could not infer GIC interrupt target ID, assuming 0.
19 available phys memory regions: 1
20   [0..40000000]
21 reserved virt address space regions: 4
22   [e0000000..e003c000]
23   [e003c000..e003ee47]
24   [e003f000..e0168000]
25   [ff000000..ff100000]
26 Booting all finished, dropped to user space
27 Component printer saying: My message.
28 Component printer saying: My message.
29 Component printer saying: My message.
30 ...

Explanation to output:

• Line 1-26: See explanation for hello-world application.
• Line 27-30: output of printer application

Now we finally come to the fun part of the tutorial and use the actual hardware. Due to availability and general support in the seL4 microkernel itself, I chose to use the Raspberry Pi 4 Model B, abbreviated with RPi4. Although QEMU is nice, if there is no emulation available for a specific board, sooner or later you have to work with the actual hardware. The following text should provide a step-by-step guide to get acquainted with the hardware and help you to setup an efficient working environment.

To continue with the tutorial, you need at minimum the following hardware components:

• laptop or desktop PC
• Raspberry Pi 4 Model B
• microSD card
• RJ45/Ethernet cable
• USB-to-UART adapter (e.g. CP2102)
• power cable

• Laptop/PC: Development host
• RPi4: Raspberry Pi 4 Model B hardware board (target machine).
• CP2102: The CP2102 USB-to-TTL adapter is used for console output through UART.
• RJ45: Ethernet cable that connects PC with hardware board to exchange files over TFTP/DHCP.
• USB-C: connect to power outlet in the wall or simply plug the cable into an ordinary USB port on the PC to power up the board
• µSD: microSD card slot -> insert an SD card that stores important (boot) files in non-volatile flash memory

A good idea when starting to prepare a development setup for a specific hardware board is to test whether the board can write on the local console. Without any textual output, it is almost impossible to work with an embedded board. This steps help to verify whether the console works for the RPi4.

Hardware Setup:

The RPi4 has in total 40 GPIO pins that allows external peripherals to interface with the processor. A console is implemented through the UART pins (GPIO 14 (TXD),GPIO 15 (RXD)) of the RPi4 as can be seen in the following graphic taken from here:

I use the CP2102 USB-to-TTL converter to provide a console for the RPi4. Other similar adapters can also be used, but the general idea is the same for all of these adapters. More information on how to connect this specific helper circuit to the RPi4 can be found under this link. For good measure, I also included the most relevant graphic below:

What is important to understand is that we connect the data lines (RX,TX) and the ground pin (GND) with the corresponding GPIO pins on the RPi4 (beware: RX and TX lines cross). The USB end of the CP2102 can be hooked into an ordinary USB port on the PC. If everything was hooked up properly, we should now be able to receive console output from the RPi4 on a local terminal window on the PC.

Console Test:

To verify the console setup, we quickly test whether everything is working properly. We use the picocom utility as terminal emulation program to provide a console for our target board. When hooking the CP2102 USB-to-TTL adapter up as described between the PC and the RPi4, you should be able to see the following output when executing the picocom command:

$ sudo picocom -b 115200 /dev/ttyUSB0
picocom v3.1

port is        : /dev/ttyUSB0
flowcontrol    : none
baudrate is    : 115200
parity is      : none
databits are   : 8
stopbits are   : 1
escape is      : C-a
local echo is  : no
noinit is      : no
noreset is     : no
hangup is      : no
nolock is      : no
send_cmd is    : sz -vv
receive_cmd is : rz -vv -E
imap is        : 
omap is        : 
emap is        : crcrlf,delbs,
logfile is     : none
initstring     : none
exit_after is  : not set
exit is        : no

Type [C-a] [C-h] to see available commands
Terminal ready

This is the normal picocom welcome screen. If you would power up the board in the current state by plugging in the power cord, the board would not print any output. The RPi4 board requires several boot files on a flash device, e.g. a microSD card.

(micro)SD card preparation:

Modern laptops/PCs typically have a microSD card slot, where our microSD card can be inserted. Before being able to boot the RPi4, we first need to properly prepare the microSD card:

1. Formatting the microSD card: The first step in preparing the microSD card is to wipe/erase all existing data from the flash device and format the card as a FAT32 partition. The gparted utility is a common Linux tool to format a flash device through a GUI.

2. Flashing the microSD card: The next step is to copy the required files to the microSD card.

Boot Files:

The RPi4 requires several official boot files that are described in RPi4 Boot Files and must be copied onto the microSD card. Therefore, copy the following files from .../resources/rpi4/ to the microSD card:

• bcm2711-rpi-4-b.dtb
• fixup4.dat
• start4.elf
• config.txt

You can now insert the flashed microSD card onto the corresponding slot on the RPi4 board, start picocom in a separate terminal and power up the board. The board should now print the following output:

...
Initialising SDRAM 'Micron' 32Gb x2 total-size: 64 Gbit 3200
recover4.elf not found
recovery.elf not found
Read start4.elf bytes  2212384 hnd 0x0000000b hash bf07104c7821ae07
Read fixup4.dat bytes     5421 hnd 0x0000000a hash 4e7be95384e3e746
0x00d03114 0x00000000 0x0000001f
MEM GPU: 76 ARM: 948 TOTAL: 1024
FIXUP src: 128 256 dst: 948 1024
Starting start4.elf @ 0xfec00200

This is the output of the board-specific boot files (primary bootloaders). But this is pretty much everything that is printed on the screen for now. What you might already noticed is that the status LED on the RPi4 blinks constantly. The board is in a pending state. What is needed next is a (secondary) bootloader, we use U-Boot.

In case you do not see the above output, there is something wrong with your setup. It can very easily happen that the cables might not be properly connected. In any case, make sure that you get console output working properly for your board, otherwise you can not proceed.

U-Boot:

We use U-Boot as our main bootloader that will later load the seL4 microkernel. We have a pre-compiled U-Boot binary in .../resources/rpi4/u-boot.bin that we will copy on our microSD card in addition to the board-specific boot files. If you want more information on how the binary was generated, you can find more information in RPi4 Boot Files. After preparing the microSD card properly, you can power up the board and get the following output:

...
U-Boot 2020.01-gea7ab14e67 (Nov 24 2020 - 21:22:28 +0100)

DRAM:  3.9 GiB
RPI 4 Model B (0xd03114)
MMC:   mmcnr@7e300000: 1, emmc2@7e340000: 0
Loading Environment from FAT... *** Warning - bad CRC, using default environment

In:    serial
Out:   serial
Err:   serial
Net:   eth0: ethernet@7d580000
Hit any key to stop autoboot:  0 
U-Boot>

You get greeted with a welcome message about the U-Boot version. Since we have no further files on our microSD card, there is no use to autoboot at the moment. If you interrupt the autoboot sequence, you fall into the U-Boot command line. You can enter U-Boot commands to interact with U-Boot. To proceed we now need the kernel image and the CapDL loader app on our microSD card.

Build Instructions:

1. Adapt the following lines in .../src/build.sh script:

BUILD_APPS_PLATFORMS=(
    "hello-world rpi4"
)

This tells the build system to build the hello-world application for the rpi4 platform.

2. Build the application:

./build.sh

As a result the kernel and CapDL loader image capdl-loader-image-arm-bcm2711 will be available in .../src/build_hello-world_rpi4/images/.

Preparation:

Copy the .../src/build_hello-world_rpi4/images/capdl-loader-image-arm-bcm2711 image onto the microSD card and rename it to os_image.bin for easier handling.

Manual Boot:

...
U-Boot> fatload mmc 0 0x10000000 os_image.bin
2596796 bytes read in 186 ms (13.3 MiB/s)
U-Boot> bootefi 0x10000000

ELF-loader started on CPU: ARM Ltd. Cortex-A72 r0p3
  paddr=[39cca000..ffffffffffffffff]
  dtb=7f00000
Looking for DTB in CPIO archive...found at 39e13668.
Loaded DTB from 39e13668.
   paddr=[23f000..245fff]
ELF-loading image 'kernel' to 0
  paddr=[0..23efff]
  vaddr=[ffffff8000000000..ffffff800023efff]
  virt_entry=ffffff8000000000
ELF-loading image 'capdl-loader' to 246000
  paddr=[246000..3cefff]
  vaddr=[400000..588fff]
  virt_entry=408e78
Enabling MMU and paging
Jumping to kernel-image entry point...

Bootstrapping kernel
available phys memory regions: 1
  [0..8000000]
reserved virt address space regions: 3
  [ffffff8000000000..ffffff800023f000]
  [ffffff800023f000..ffffff80002454f4]
  [ffffff8000246000..ffffff80003cf000]
Booting all finished, dropped to user space
Hello CAmkES World

We now power up the target board and drop into the U-Boot command line. So far nothing new. Since we have the os_image.bin image on the microSD card now, we can now start our kernel image through the command line. We first load the os_image.bin image at location 0x10000000 from a FAT filesystem of our microSD card into memory (U-Boot command fatload ...). Then we launch our loaded kernel image that is located at 0x10000000 in memory (U-Boot command bootefi). Afterwards the seL4 kernel and our application are started as we saw in the QEMU case.

Automated Boot:

Always dropping into the U-Boot command line to manually load and execute the binary image is unnecessarily complicated. U-Boot allows to automate this process through a boot script (boot.scr). We basically enter the commands we would enter on the U-Boot command line into a boot.cmd file and transform it into the boot.scr binary file as described in RPi4 Boot Files. U-Boot loads this file during bootup if available and executes the corresponding commands.

If you don't want to generate the boot.scr file yourself, you can load the boot script in .../resources/rpi4/sd_boot/ onto the microSD card. This time when booting the board, you should receive the following output:

...
Hit any key to stop autoboot:  0 
switch to partitions #0, OK
mmc0 is current device
Scanning mmc 0:1...
Found U-Boot script /boot.scr
129 bytes read in 16 ms (7.8 KiB/s)
## Executing script at 02400000
2596796 bytes read in 186 ms (13.3 MiB/s)
Card did not respond to voltage select!
Scanning disk [email protected]...
Disk [email protected] not ready
Scanning disk [email protected]...
Found 2 disks

ELF-loader started on CPU: ARM Ltd. Cortex-A72 r0p3
  paddr=[39cc9000..ffffffffffffffff]
  dtb=7f00000
Looking for DTB in CPIO archive...found at 39e12668.
...

As you can see this time we do not drop into the U-Boot command line but U-Boot finds our boot.scr script and executes the corresponding U-Boot commands. As a result, we get our expected output.

Although we are able to automate the boot flow through the boot script boot.scr, we still have one major bottleneck in our development workflow. Every time we want to update our kernel image os_image.bin, we have to flash our microSD card with the newly compiled binary first. This might be acceptable during our setup, but when repeatedly testing our application, this becomes a real overhead. To deal with this problem, we can use network boot through TFTP/BOOTP.

Concept:

Everytime our board starts up, we want to pull our os_image.bin from the host to the target board to cut development time. To realize this, we need to setup a DHCP and TFTP server on our host and configure it to pass the os_image.bin binary to the target board, which will be our DHCP/TFTP client. The DHCP server is used to hand out a dynamic IP address to the RPi4 (we could theoretically also give the board a static IP address, but DHCP provides a more flexible/scalable approach). The TFTP server runs as a daemon and listens for incoming requests to provide the necessary files to the RPi4.

Host Configuration:

1. Set up a TFTP server according to TFTP Boot. Don't forget to copy .../src/build_hello-world_rpi4/images/capdl-loader-image-arm-bcm2711 to TFTP directory and rename it to os_image.bin.

2. Add 192.168.137.1 server ip address on the ethernet port that is connected to the board:

sudo ip addr add 192.168.137.1/24 dev <eth-port>

3. Configure a DHCP server to hand out IP addresses to a DHCP client and configure the TFTP/BOOTP options to hand out our kernel binary os_image.bin through TFTP:

sudo dnsmasq -p 0 -i <eth-port> -F 192.168.137.50,192.168.137.100,255.255.255.0 -M os_image.bin

We disable DNS function (-p 0), listen only on the <eth-port> (-i <eth-port>), enable the DHCP server to hand out ip addresses to a DHCP client between 192.168.137.50 and 192.168.137.100 (-F ...) and set the BOOTP/TFTP options to be returned by the DHCP server, more precisely the os_image.bin filename for network boot (-M os_image.bin).

4. Plug ethernet cable between laptop and RPi4 in order to allow network packets to be transmitted between host and target.

Target configuration:

After setting up DHCP, TFTP and network interface on our host, we can power up our board and drop into the U-Boot command line. Before we can utilize the network boot, we configure U-Boot on the RPi4 as follows:

...
U-Boot> setenv serverip 192.168.137.1

This sets the IP address of the host (serverip) which is running TFTP and NFS servers.

Manual Boot:

After manually configuring U-Boot for our target board, we can now execute the remote network boot as follows:

...
U-Boot> dhcp 0x10000000
BOOTP broadcast 1
BOOTP broadcast 2
BOOTP broadcast 3
BOOTP broadcast 4
DHCP client bound to address 192.168.137.90 (3022 ms)
Using ethernet@7d580000 device
TFTP from server 192.168.137.1; our IP address is 192.168.137.90
Filename 'os_image.bin'.
Load address: 0x10000000
Loading: #########################T ##############################T ##########
	 ##################T ###############################################
	 ###############################################
	 162.1 KiB/s
done
Bytes transferred = 2596796 (279fbc hex)
U-Boot> bootefi 0x10000000
Card did not respond to voltage select!
Scanning disk [email protected]...
Disk [email protected] not ready
Scanning disk [email protected]...
Found 2 disks

ELF-loader started on CPU: ARM Ltd. Cortex-A72 r0p3
  paddr=[39cca000..ffffffffffffffff]
  dtb=7f00000
Looking for DTB in CPIO archive...found at 39e13668.
...

We first instruct our board to contact the DHCP server on the host to hand out an IP address for the board and afterwards load the kernel image to address 0x10000000 (dhcp 0x10000000). This works because we configured the host correspondingly. Afterwards we launch the loaded binary from location 0x10000000 (bootefi 0x10000000). Afterwards, the usual boot sequence starts.

Automatic Boot:

Similar to the microSD card boot, we can also create a boot script for the TFTP boot. An exemplary boot script can be found under .../resources/rpi4/tftp_boot/boot.scr. Copy this file onto the microSD card and power up the board. You should receive the following output:

...
Hit any key to stop autoboot:  0 
switch to partitions #0, OK
mmc0 is current device
Scanning mmc 0:1...
Found U-Boot script /boot.scr
137 bytes read in 16 ms (7.8 KiB/s)
## Executing script at 02400000
ethernet@7d580000 Waiting for PHY auto negotiation to complete... done
BOOTP broadcast 1
BOOTP broadcast 2
DHCP client bound to address 192.168.137.90 (267 ms)
Using ethernet@7d580000 device
TFTP from server 192.168.137.1; our IP address is 192.168.137.90
Filename 'os_image.bin'.
Load address: 0x10000000
Loading: #################################################################
	 #################################################################
	 ###############################################
	 5.4 MiB/s
done
Bytes transferred = 2596796 (279fbc hex)
Card did not respond to voltage select!
Scanning disk [email protected]...
Disk [email protected] not ready
Scanning disk [email protected]...
Found 2 disks

ELF-loader started on CPU: ARM Ltd. Cortex-A72 r0p3
  paddr=[39cc9000..ffffffffffffffff]
  dtb=7f00000
Looking for DTB in CPIO archive...found at 39e12668.
...

If we do not interrupt autoboot to drop into the U-Boot command line, U-Boot loads the boot.scr into memory and executes the commands as specified before. As a result, the board will automatically configure the serverip, contact the DHCP server and pull the os_image.bin binary from the host over TFTP. Afterwards, the usual boot sequence starts.

If you completed the entire tutorial, you learned how to use our OS framework and set up an efficient development workflow for the RPi4 hardware board. We first introduced a virtualized development workflow based on QEMU. This is really handy if you have no access to any hardware board and simply want to test an ARM application, there is a high probability that the application will behave similar on a real ARM hardware board. Afterwards, we showed you step-by-step how to set up a development workflow for the RPi4 hardware board. It is always recommended to first do the manual boot cases during testing before using the automated boot scripts. When everything is setup, you can now really efficiently test your applications.

You can keep experimenting with the current version of the OS framework, but the functionality is quite limited as I simply wanted a practical project to showcase some common embedded development knowledge. Some ideas on how to proceed:

• Add more applications or CAmkES components
• Add another hardware board
• Improve the CI/CD pipeline to include actual hardware boards instead of only the Zynq7000 case
• Add a hardware debugger to the RPi4
• ...

Thank you for reading the tutorial. I hope it was helpful.