On Sat, Mar 7, 2015 at 6:18 AM, Sebastian Lau <[email protected]> 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 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_Process 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. But please correct me, if I'm wrong. _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
