Am 07.03.2015 um 13:00 schrieb Wolfgang Keller: > 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 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_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. 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 > [email protected] > https://sel4.systems/lists/listinfo/devel -- Robert Kaiser Computer Engineering RheinMain University of Applied Sciences _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
