Re: [seL4] A port to the Raspberry Pi 2?

Am 07.03.2015 um 13:00 schrieb Wolfgang Keller:

On Sat, Mar 7, 2015 at 6:18 AM, Sebastian Lau wrote:

...

Would a port of seL4 to the raspberry pi 2 be welcome because I'm interested in buying a raspberry pi 2 and building sel4 for it? I have not much knowledge about seL4, but the boot process of the RPi (all versions) is rather special:

On Raspberry Pi, it's not the ARM core that boots, but the GPU starts executing a bootloader that is stored in ROM. At that moment SDRAM and the ARM core is disabled. The first stage bootloader's only purpose is reading bootcode.bin from the SD card into the L2 cache.

The 2nd stage bootloader (boot/bootcode.bin) also runs on the GPU. Its purpose is enabling the SDRAM and loading the GPU firmware (in most cases boot/start.elf). This is a OS in itself based on ThreadX running on the GPU and thus a large binary blob. It reads a few settings, enables the ARM core and starts it executing boot/kernel.img. Only from this point on, Linux starts booting. I don't think bootstrapping would be that much of a problem. The trick would be to provide a kernel.img that contains U-boot instead of Linux at this point. Once U-boot is in control, it should be possible to boot seL4 with it. AFAIK, there is support in mainline U-boot for the Raspberry Pi already.

I hope I don't have to mention that the instruction set itself for start.elf is not documented...

References:

http://wiki.beyondlogic.org/index.php?title=Understanding_RaspberryPi_Boot_P... http://www.raspberrypi.org/forums/viewtopic.php?f=63&t=6685 http://raspberrypi.stackexchange.com/a/10595/9138 (a little outdated, now loader.bin is not used anymore)

Since the ARM core is just a slave to the GPU core which runs a binary blob based on ThreadX, this makes it IMHO very difficult to apply the correctness proof and guarantees of seL4 to the RPi version. If you can relinquish the correctness guarantees of seL4 (the thing that makes seL4 interesting), I think porting seL4 to the RPi2 should be in principle doable.

IMHO, the biggest problem with the Raspberry Pi is that most of its I/O (even the NIC) is connected through USB. A serial port is available (albeit without level shifters). So, running the seL4test should be possible without a USB stack, but as soon as you want to access a keyboard, network or filesystem, you'll need one. @Sebastian: I had a plan of porting seL4 to Rasperry Pi myself whenever I find the Time (TM), so I'd be more than happy if you could do this. My plan was to look at the Fiasco.OC kernel from Dresden: it does support the Raspi, so it may helpful to look at that code. Robert

But please correct me, if I'm wrong.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

-- Robert Kaiser Computer Engineering RheinMain University of Applied Sciences