seL4 now runs on Pi3

Very recently, we(the Trustworthy Systems group) merged Raspberry Pi 3 support for seL4. This excellent blog post by Kofi already highlights why this is great news. Personally, it is exciting because, a Raspberry Pi 3 is a lot more accessible than all the other boards we’ve previously ran our kernel on. I own one too, and it is absolutely amazing that I can run, muck around and put my Raspberry Pi 3 to some good use. I’ve been playing around with seL4 on my Pi3. The things that I’m currently trying to do are:

  • Get Haskell runtime on seL4. Some might say this is an exercise in futility, but this will help me get Cogent build on seL4, and then I can start building verified systems software(currently file systems) on top of seL4. Ofcourse, this involves a lot more than just the filesystem implementation(need a VFS layer, block cache, drivers etc.). It might be a long shot, but hey, I’m trying!
  • The OS that I’ve been trying to build, forever(Who hasn’t tried to build one, really?). With seL4, the kernel is taken care of, letting us build all the fun stuff on top(Students of the AOS class at UNSW do exactly this).

Good times!

4 thoughts on “seL4 now runs on Pi3

      • Hi, Thank you for replying.
        I am able to get u-boot working.
        But when i try to load u-boot.bin corresponding to sel4 image it stops at application loading at 0x02000000.
        I am using the commands as follows:
        fatload mmc 0 ${loadaddr} u-boot.bin
        go ${loadaddr}

        Sd card contains the following:-
        u-boot.bin
        config.txt
        sel4test-driver-image-arm-bcm2837
        start.elf
        bootcode.bin

        Are there any particular set of commands that we should follow after u-boot prompt

  1. Hi Partha,
    I am elaborating the procedure I have followed:
    Steps followed for bootabe image
    1. mkdir sel4test && cd sel4test
    2. repo init -u https://github.com/seL4/sel4test-manifest.git
    3. repo sync
    4. make rpi3_debug_xml_defconfig && make
    seL4 bootabe image is generated with the filename “sel4test-driver-image-arm-bcm2837 ”
    Then for u-boot, following steps are executed
    1. git clone git://git.denx.de/u-boot.git u-boot-git && cd u-boot-git
    2. make CROSS_COMPILE=arm-linux-gnueabi- distclean
    3. make CROSS_COMPILE=arm-linux-gnueabi- rpi_3_32b_defconfig
    4. make CROSS_COMPILE=arm-linux-gnueabi- u-boot.bin
    The SD card have following files:
    1. bootcode.bin
    2. start.elf
    3. fixup.dat
    4. config.txt (kernel=u-boot.bin enable uart=1)
    5. sel4test-driver-image-arm-bcm2837
    6. bcm2837-rpi-3-b.dtb
    7. cmdline.txt
    I have U-boot working with these files
    Steps to load sel4kernel image:
    1. fatload mmc 0:1 ${loadaddr} sel4test-driver-image-arm-bcm2837
    2. bootelf ${loadaddr}
    After this I get the following errors
    CACHE: Misaligned operation at rangee [200030c8, 20003218]
    CACHE: Misaligned operation at rangee [20003218, 20003564]
    CACHE: Misaligned operation at rangee [20003564, 20003760]
    ….
    ….
    CACHE: Misaligned operation at rangee [200a4000, 200b4820]
    ## Starting application at 0x20000000
    And then it stops at this line and does not boot the kernel.

    Can you please guide me about why I am getting this error. Also is it required to load bcm2837-rpi-3-b.dtb at fdt_addr_r?

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s