seL4 in GLAS

This document desribe the procedure to run seL4 in GLAS on Morello FVP.

Prerequisite

Setup the Kirsch toolchain container - see Acquiring the Kirsch Toolchain.

Prepare the workspace

Multiple repos are required for this project. Prepare a folder as your workspace. This folder will be shared with the Kirsch Docker container later.

1. Clone seL4 (our version) as sel4.

Note

To boot the second kernel in the low memory (staring 0x80000000), we need to mark the later part of the region invisible to seL4. In this case, use branch limited-ram-for-sel4, where seL4 sees RAM size 0x40000000.

2. Clone seL4 Microkit (our version) as sel4-microkit.

3. Clone the main repo as sel4-in-glas.

Compile the seL4 Microkit

Enter the toolchain container with the workspace mapped to \src:

docker run --mount type=bind,source=$(pwd),target=/src --rm -ti registry.ethz.ch/project-opensockeye/kirsch-toolchain /bin/bash

Inside the container shell:

cd /src/sel4-microkit
python3 -m venv pyenv
./pyenv/bin/pip install --upgrade pip setuptools wheel
./pyenv/bin/pip install -r requirements.txt

The following command build the Microkit for Morello FVP platform:

PATH="/tools/arm-gnu-toolchain/bin:$PATH" ./pyenv/bin/python3 build_sdk.py --sel4="../sel4" --filter-boards morello_fvp --no-doc --no-archive --tool-rebuild

Note

To build more boards such as qemu_arm_virt, supply more options to --filter-boards. See build_sdk.py for available boards. Not all boards can be built or work. For example, the RISC-V ones currently cannot be built without the RISC-V toolchain.

Note

If only seL4 is modified, removing --tool-rebuild can save some build time. However, if Microkit script is modified, --tool-rebuild is needed.

The built SDK is in /src/sel4-microkit/release/microkit-sdk-1.2.6.

Target: wordle_part3

This target launches seL4 with Wordle programs (wordle_part3.system) as well as booting helloworld/helloword.c on a second core.

Inside the container, in /src/sel4-in-glas, run make run_wordle_part3. Alternatively, outside the container, at your workspace:

docker run --mount type=bind,source=$(pwd),target=/src --rm -ti registry.ethz.ch/project-opensockeye/kirsch-toolchain make -C /src/sel4-in-glas run_wordle_part3

Note

The ATF build assets are left inside the container. To save time building it, consider using a persistent contaienr.

In the output, you should see the following:

# ATF
NOTICE:  Booting Trusted Firmware
...
# seL4 loader
LDR|INFO: Flags:                0x0000000000000001
            seL4 configured as hypervisor
LDR|INFO: Kernel:      entry:   0x0000008080000000
...
LDR|INFO: region: 0x00000008   addr: 0x0000000080269000   size: 0x0000000000001070   offset: 0x000000000026c2f0   type: 0x0000000000000001
LDR|INFO: region: 0x00000009   addr: 0x00000000f0000000   size: 0x0000000000000349   offset: 0x000000000026d360   type: 0x0000000000000001
# This last region is the binary for the second kernel
...
LDR|INFO: Boot CPU ID (0x00000000)
LDR|INFO: PSCI version 0x00010001
LDR|INFO: Boot the secondary kernel (entry 0x00000000f0000000) on CPU ID (0x00000100)
LDR|INFO: enabling MMU
****************************************
Hello world from CPU 0x00000100 at EL2
****************************************
LDR|INFO: jumping to kernel
# seL4 kernel
Bootstrapping kernel
...
# User programs
SERIAL SERVER: starting
WORDLE SERVER: starting
CLIENT: starting
Welcome to the Wordle client!
[ ] [ ] [ ] [ ] [ ]
...
# The answer is "hello"

The console is connected to telnet. To exit, use Ctrl + ] quit.

Target: virtio_blk

This target generates a random 5K file as bin/virtio_blk.load.bin, runs the virtio-blk server and a demo client to read and print all its content (virtio_blk.system).

docker run --mount type=bind,source=$(pwd),target=/src --rm -ti registry.ethz.ch/project-opensockeye/kirsch-toolchain make -C /src/sel4-in-glas run_virtio_blk

Target: vmm_minimal

This target launches a minimal VM on Morello FVP (vmm_minimal.system).

docker run --mount type=bind,source=$(pwd),target=/src --rm -ti registry.ethz.ch/project-opensockeye/kirsch-toolchain make -C /src/sel4-in-glas run_vmm_minimal

Note

The VM images (kernel, DTB, initrd) are loaded through virtio-blk becuase ATF FIP cannot handle large BL33 that has images embedded. So far we haven’t found a way to load data directly into the Morello FVP main memory (--data does not work, possibly due to the tagged memory?). The loading can take several minutes.

Target: demo

This demo launch demo.c (demo.system) as well as booting cheriette_morello_loader.bin on a second core.

Note

cheriette_morello_loader.bin is not part of sel4-in-glas repo. You need to add it manually. If using .bin instead of .elf, the kernel entry address need to be specified in the Makefile.

To build Cheriette for the seL4 GLAS demo, generate the build script with python3 generators/build.py --demo-enable True > build/build.ninja, and build the Morello target ninja -C build morello_all. Then, copy build/loader_morello.bin to the sel4-in-glas directory as cheriette_morello_loader.bin.

Inside the container, in /src/sel4-in-glas, run make demo. Alternatively, outside the container, at your workspace:

docker run --mount type=bind,source=$(pwd),target=/src --rm -ti registry.ethz.ch/project-opensockeye/kirsch-toolchain make -C /src/sel4-in-glas run_demo

Target: clean

docker run --mount type=bind,source=$(pwd),target=/src --rm -ti registry.ethz.ch/project-opensockeye/kirsch-toolchain make -C /src/sel4-in-glas clean

Tracing

To enable tracing on target wordle_part3, use target trace_wordle_part3. The same applies to other targets.

In the code, trace starts after asm volatile ("hlt 0x1" ::: "memory");. Insert this code to the desirable place. Note that executing this instruction without tracing enabled results in an error.

The trace is stored in logs/trace.log. It can be very long, you may want to use command like cat logs/trace.log | tail -n +200000 | head -n 100000 > trace_part.log to skip the first 200000 lines and take 100000 lines, before you open the whole file.

Note that tracing will significantly slow down execution!