Am 10.03.2015 um 01:56 schrieb da Tyga:

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.

You should keep in mind that seL4 is a microkernel. So the USB stack and drivers that depend on that stack should all be implemented as processes/tasks running on top of seL4.

Sure.

Nevertheless, for debug purposes at least, even seL4 uses a serial channel of some kind. Luckily for any seL4 porting effort, the Raspi has a UART and it is accessible directly, not through USB. Otherwise the microkernel would have to handle USB...

I know it is not cool to mention Minix here, but it and Plan9 suggest ideas as to how the layers above seL4 could be structured.

I believe NICTA and others have been/are actively working on that.

As far as I can understand, seL4 is not an operating system, it is a microkernel upon which one or more operating systems could be built. The key reason to use seL4 would be due to it providing capabilities based isolation between the layers that run on top of it and thus preventing rogue processes from interfering with other processes.

In the context of "one or more" operating systems, the question arises how to deal with shared resources, such as a USB stack. Imagine multiple OSes handling different USB devices which are all physically connected to the single USB host controller of a Rasperry Pi. What should be the position of the USB stack in this case? We agreed that it should not be in the microkernel. SInce it has to be shared, it can not be part of any one of the OSes. So it would have to exist as a self-contained component (a "server" if you will). But then, how should it be controlled/configured and where does it get its resources from?

Similar thoughts apply to a network stack and, in the case of the Raspi, the NIC is accessed through USB, so we end up with a shared component (networking) on top of another shared component (USB). Tricky...

Robert

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

-- 
Robert Kaiser

Computer Engineering
RheinMain University of Applied Sciences