Hardware Platform for sel4 and running linux as guest os
Dear all, I am looking to purchase a board for a project that will use sel4. I have the following hardware requirements: - serial port - ethernet - potentially usb Then, I want to run linux on top of sel4 and have also some native components. In the linux partition, I would like to control the usb and potentially the ethernet. In the native components, I am planning to use the serial port (communication with other components). I thought the beagleboard black would be a good match. Does anyone tried to run linux as a guest os on this platform? If yes, is there any tutorial/example to set it up? Also, any information about how to use the serial ports and other hardware components? Also, if you have an experience with any other board (x86 or ARM - the platform does not really matter), is it possible to indicate what you would recommend? Thanks for any help or suggestion, Julien.
Hi Julien, I can confirm from experience that seL4 supports both serial and ethernet on the FreeScale Sabre Lite i.MX6 board (although through some buggy, GPL'd, drivers for ethernet). No idea about USB nor running Linux on top of seL4. Cheers, -Andrea On Sat, Jan 2, 2016 at 10:18 AM, Julien Delange <julien.delange@gmail.com> wrote:
-- Andrea Sorbini Software Engineer asorbini@rti.com +1.408.990.7475 www.rti.com RTI - Your systems. Working as one.
"Andrea" == Andrea Sorbini <asorbini@rti.com> writes:
Andrea> I can confirm from experience that seL4 supports both serial Andrea> and ethernet on the FreeScale Sabre Lite i.MX6 board (although Andrea> through some buggy, GPL'd, drivers for ethernet). No idea Andrea> about USB nor running Linux on top of seL4. For running virtualised environments, you need a platform with the ARM virtualisation extensions -- a Cortex A53, A15 or A7. Our preferred platform was the Odroid XU; as this has been discontinued, we're looking around for a different readily available platform, preferably with a System MMU to protect all DMA. It's looking like the Nvidia Tegra TK1 will be apropriate, but we haven't started the port yet. -- Dr Peter Chubb Tel: +61 2 8306 0552 http://www.data61.csiro.au http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA/Data61
I think the only thing you can't do in linux is manage the MMU, since sel4 reserves that task to itself (plus it's a ring 0 operation and sel4 IIRC runs guests, even the linux kernel, as ring 3) What I'm not so sure about is I/O capabilities. Does seL4 require a system call to do I/O or can seL4 manipulate a task's IO permission bitmap? If the former, I think you could tie an exception handler to the linux kernel and use that to emulate any privileged opcodes. On Mon, Jan 4, 2016 at 1:35 PM, Julien Delange <julien.delange@gmail.com> wrote:
On Sat, Jan 2, 2016 at 10:18 AM, Julien Delange <julien.delange@gmail.com> wrote:
<https://sel4.systems/lists/listinfo/devel>The BBB does have a way to run from a uSD card as does the latest Raspberry Pi. The programming and tools on the Raspberry Pi seem a bit richer. The BBB environments want to program the flash memory and that can take a long time. There are some developer tricks to null it out and boot from a uSD quickly. The R-Pi will boot a new uSD card image quickly. The new R-Pi has an abundance of USB ports so you can boot an OS on the uSD card and load a spare uSD image on a card mounded on an adapter. This allows quicker development test cycles. Start with the bootstrap code and have it load a sel4 image (not vmlinux). It is necessary to have enough support in sel4 to manage (start/stop) your hosted OS. Since the new R-Pi is multi core you can address MP or constrain yourself to one single core. Multiple cores have value if you want and OS to be supervised. Both are interesting and I have both -- the R-Pi seems to be the best supported at many levels with some foot notes. http://www.xenproject.org/help/questions-and-answers/raspberry-pi-on-xen.htm... http://blog.flexvdi.com/2015/02/25/enabling-hyp-mode-on-the-raspberry-pi-2/ this next tells me that interrupts are a hardware problem. http://www.gossamer-threads.com/lists/xen/users/369667 -- T o m M i t c h e l l
I did all my beaglebone black development from a remote ubuntu desktop and tested images using netboot and a serial console. The netboot was slightly slow but it avoided having to write any flash or sd cards, and I didn't have to constantly boot into and out of a dev environment. Instructions for netbooting sel4 on the bbone black are on the website: https://sel4.systems/Info/Hardware/Beaglebone/ On Wed, Jan 6, 2016 at 3:01 PM, Tom Mitchell <mitch@niftyegg.com> wrote:
-- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com
participants (6)
-
Andrea Sorbini -
Julien Delange -
Peter Chubb -
Raymond Jennings -
Tim Newsham -
Tom Mitchell