...

...

...

...

"Andrea" == Andrea Sorbini 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 wrote:

So, there is no chance for running linux on top of sel4 on a beagleboard black?

On Mon, Jan 4, 2016 at 4:30 PM, Peter Chubb wrote:

...

...

...

...

...

> "Andrea" == Andrea Sorbini 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

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

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 wrote:

On Sat, Jan 2, 2016 at 10:18 AM, Julien Delange wrote:

...

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.

https://sel4.systems/lists/listinfo/develThe 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

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

-- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com