Hi,

I am posting this email as reference to anyone who want/need to run seL4 on a BeagleBone Black (BBB).

The post at https://wiki.sel4.systems/Hardware/Beaglebone is great, unfortunately even if I followed exactly those instructions, I ended up hitting some walls here and there.

I eventually managed to solve those issues and run successfully seL4test on my BBB.

First of all the build system. I have tried unsuccessfully to find arm-linux-eabi for CentOS 7 (my preferred distribution for building on Linux), but apparently is an easy-to-find only on Ubuntu... so I ended up creating a VM with Ubuntu 16.04. If someone knows how to get arm-linux-eabi on CentOS please let me know...

Unfortunately even with Ubuntu not everything went as smooth as I hoped.

It appears that Python "past" module is no longer available for 16.04, so build fails on kernel/tools/lex.py.

According to the comment right before the failing import statement, it appears this module is just declared but not used, so commenting it out (or removing it entirely) would fix this issue:

#from past.builtins import cmp

One more issue: when using either one of the following configurations as start point:
- bamboo_bbone_black_debug_xml_defconfig

- bbone_black_debug_xml_defconfig

The build system will end up producing a binary image and not an ELF image. Producing an ELF image can be more useful if you want to use objdump to get a disassembly (for debugging later).

So I changed the configuration with:

make menuconfig

Navigate to:

Tools -> Build elfloader -> Boot image type

and select "ELF Boot Image" instead of "Binary Boot Image"

Save your configuration then build:

make

Now manually convert the produced ELF image in a binary:

arm-linux-gnueabi-objcopy --output-target binary images/sel4test-driver-image-arm-am335x sel4test.bin

then copy the file 'sel4test.bin' onto the SD card formatted as FAT32

Now, in my BBB (rev A5A) if I try to follow the instructions from the wiki page previously mentioned, I get a crash right away (illegal instruction).

The problem is that in my BBB the uBoot environment variable ${loadaddr} is set to 0x80200000 and not 0x82000000 (the start address of the produced image).

BBB have RAM mapped from address 0x80000000 to 0x9FFFFFFF (512Mb), so running from 0x82000000 is ok.

So to load and run, use instead:

fatload mmc 0 0x82000000 sel4test.bin

go 0x82000000

That's it. Test should load and run successfully:

Test suite passed. 220 tests passed.

220/220 tests passed.
All is well in the universe.

Hope this help saving some time...

Regards,

Fabrizio