- Devel - lists.sel4.systems

Using Rump kernels to run unmodified NetBSD drivers on seL4
by Kent.Mcleod＠data61.csiro.au 06 Mar '17

06 Mar '17

Last year for my honors thesis I evaluated rump kernels as a way of running unmodified NetBSD drivers on seL4. This work has recently been pushed out with a corresponding blog post: https://research.csiro.au/tsblog/using-rump-kernels-to-run-unmodified-netbs…. This was done by adding support for the Rumprun unikernel to use seL4 as a target platform. Currently ia32 and x86_64 is supported and we have tested the e1000 network card driver and networking stack using Dell Sandy Bridge and Haswell machines. Rump kernels are a project that allows unmodified NetBSD OS component reuse in other systems (http://rumpkernel.org/) We want to use rump kernels as a way of providing drivers and other OS components such as filesystems and networking stacks on seL4 such as in CAmkES components. Some sample applications can be found here (https://github.com/SEL4PROJ/rumprun-sel4-demoapps) and a link to the thesis can be found here (http://www.disy.cse.unsw.edu.au/theses_public/16/kentm.pdf) Kent McLeod

2 1

ARM timer driver and interrupts
by Wladislav Wiebe 28 Feb '17

28 Feb '17

Hello, I wrote a new timer driver for this timer device: http://www.ti.com/lit/ug/sprugv5a/sprugv5a.pdf I am already able to run the seL4 testsuite successfully, except the interrupt/timer tests. It waits forever @ wait_for_timer_interrupt(env); I've uploaded the driver temporary to: https://github.com/wwladikw/devel/blob/master/timer.c Any idea what could be wrong? I am able to run the timer periodically or as oneshot. The gic_390 interrupt driver in the kernel should also be compatible with the gic_400, for my understanding, right? The SoC I am using contains a Coretex A15. Thanks a lot in advance! Wladislav Wiebe

3 9

Boot Hyp mode in elfloader
by SHI, Yao 27 Feb '17

27 Feb '17

I am trying to boot CAmkES-ARM-VM and got problem in elfloader. I tested Jetson-TK1 and TK1-SOM. The results are same. I've set bootm_boot_mode=nonsec in u-boot and tracked registers in function switch_to_hyp_mode(). 1) Enter switch_to_hyp_mode(), after asm volatile ("mrc p15, 0, %0, c1, c1, 0":"=r"(scr)); ==> scr == 0x100, in which NS==0, HCE==1, SCD==0, SIF==0 2) Then switch_to_hyp_mode() changes NS to 1, so scr==0x101 asm volatile ("mcr p15, 0, %0, c1, c1, 0"::"r"(scr)); 3) switch_to_hyp_mode() changes cpsr to Hyp mode asm volatile ("cps %0\n\t" "isb\n" ::"I"(HYPERVISOR_MODE)); 4) The final step, switch_to_hyp_mode() reads cpsr, asm volatile ("mrs %0, cpsr":"=r"(scr)); ==> scr == 0x6000001da, in which cpsr.M==0x1a, cpsr.I==1, cpsr.F==1, cpsr.A==1 Finally, the process died here. My questions are, 1) Are NS==0 and HCE==1 correct when entering switch_to_hyp_mode() ? 2) Is the final status (cpsr.F==cpsr.I==cpsr.A==1) expected? 3) Any other mistake I might make? Yao

2 4

Clarification on seL4 on RPi3b
by Joseph Adam Powers 23 Feb '17

23 Feb '17

It seems to be necessary for me to use the debug output using a serial cable on UART0 u-boot seems to be waiting for a Ethernet or serial cable connection to finish boot process. I don't have the serial cable so I just need some understanding that that is the case considering that I followed the rest of the instructions on the blog at https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ , newbie question btw.

2 1

RT and domains
by rad021993＠yandex.ru 21 Feb '17

21 Feb '17

Hi, Could you tell me why did you not implement domains in RT kernel version? Are there any difficulties? I'm going to add support of domains, and at the first sight I don't see any difficulties.

3 3

seL4 no longer support zynq7000 board?
by wang 21 Feb '17

21 Feb '17

Hello, https://wiki.sel4.systems/Hardware On this seL4wiki hardware page I find the link of Zynq7000 turns grey, and the page says "This page does not exist yet. You can create a new empty page, or use one of the page templates." So it means seL4 do not support zynq7000 any more? And how can I run seL4/seL4test on zynq7000 board? Thanks!

2 1

seL4/seL4test on odroid-xu4
by wang 17 Feb '17

17 Feb '17

Hello, I've just got my odroid-xu4 board and tried to port seL4test onto it, but met some problems that cannot procceed. Do you have any guide or tutorial for it step by step? I think I may have problem of initializing and partitioning of a new sd card(main problem?). And maybe something is wrong with the uboot or fastboot, but I'm not quite sure about that. This is my fist time using this devel, don't know whether this message was sent correctly or not :) Looking forward to get some help by you guys. Thanks! Wang

1 0

seL4/seL4test on odroid-xu4
by wang 17 Feb '17

17 Feb '17

Hello, I've just got my odroid-xu4 board and tried to port seL4test onto it, but met some problems that cannot procceed. Do you have any guide or tutorial for it step by step? I think I may have problem of initializing and partitioning of a new sd card(main problem?). And maybe something is wrong with the uboot or fastboot, but I'm not quite sure about that. This is my fist time using this devel, don't know whether this message was sent correctly or not :) Looking forward to get some help by you guys. Thanks! Wang

1 0

camkes DMA with predetermined physical addresses
by Gareth Howard 17 Feb '17

17 Feb '17

1 0

Deriving and Revoking IRQControl caps
by Andrew Gacek 16 Feb '17

16 Feb '17

Based on the seL4 manual it sounds like IRQControl caps only support one level of derivation. What is the reason for this restriction? We encountered a case where we wanted to hand out an IRQControl for a specific irq and then later revoke access, but we couldn't do it because the IRQControl for a specific irq is already a derived capability. -Andrew

5 10