I recently got sel4test for seL4 11.0.0 to run on my pinebook pro and I thought I would share how I did it.
Configure and build sel4test
mkdir sel4test cd sel4test repo init -u https://github.com/seL4/sel4test-manifest.git -b refs/tags/11.0.0 repo sync mkdir build cd build ../init-build.sh -DPLATFORM=rockpro64 -DSIMULATION=FALSE ninja
Convert the generated elf file to a u-boot image
The image created by the rockpro64 build script doesn’t work on the pinebook pro. I’m not sure if this is because the pinebook pro is different than the rockpro64 board or if something isn’t configured correctly in the build script.
To generate the correct image, run this from your build/images directory:
../../tools/seL4/cmake-tool/helpers/make-uimage /usr/bin/aarch64-linux-gnu-objcopy ../elfloader/elfloader arm64 sel4test-driver-image-arm-rockpro64-uboot
Deploy the image to a bootable sd card
The pinebook pro bootloader makes this easy for us, we just need to create the right files on the sdcard. I created a partition on my sd card and formatted it as the FAT file system.
timeout 10 default SEL4TEST menu title sel4test label SEL4TEST kernel /sel4test-driver-image-arm-rockpro64-uboot fdt /kernel.dtb
From your build directory, copy these files to the root of your sdcard:
Run on the pinebook pro
Follow the procedure on the pinebook pro wiki to enable the serial port and set up your terminal on the host computer.
CAUTION: The USB-to-serial-earphone-plug device sold on the pine store is the incorrect voltage (5V) for the pinebook pro, which requires 3.3V. Using it could damage your device.
Note also that the sdcard port on the pinebook pro isn’t aligned perfectly with the case – if you’re not careful you could insert the sdcard above the port and get it stuck between the case. Best to angle it slightly downwards as you insert it, and verify you encounter some resistance from the spring once you get it almost inserted before pushing it in all the way.
Insert the sdcard into the pinebook pro, reboot, and it should load up sel4test for you.
Other things I noticed
There is a build error when enabling SMP in the 11.0.0 release. This has been fixed in the master branch.
sel4test freezes while testing SMP IPC when SMP is enabled with all 6 cores. It succeeds if only 4 cores are enabled.
The rockpro64 platform does not build with ARM_HYP enabled.