Running sel4test on the pinebook pro (rockpro64)

seL4 kernel
1

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.

  1. 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

  2. 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

  3. 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.

    • Create /extlinux/extlinux.conf:

      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:

      • images/sel4test-driver-image-arm-rockpro64-uboot
      • kernel/kernel.dtb

  4. 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.