March 2017 - Devel - lists.sel4.systems

TK1 VMM SMMU Translation Error
by Enrique Leon 14 Mar '17

14 Mar '17

Hello All, We have recently run into an issue trying to boot the TK1 VMM on a TK1 Jetson board. The kernel tries to run but soon runs into translation errors after a couple of seconds. We are using the non-secure dtb with the initrd image. Here are some of the lines, it continues on like this and never stops. SMMU Address translation error: ID: 1 address: 0x0 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 SMMU Address translation error: ID: 1 address: 0x18fc00 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x SMMU Address translation error: ID: 1 address: 0x912c0 type: 6 direction: 0x0 We had success running the VM using the previous commit from camkes-arm-vmm repo, but the newest commit has introduced this issue. We have isolated it to line 93 in the "vmm_common.camkes" file. Removing "0x54200000:18", // Display A" from the file fixes the problem and we can boot as normal. We are also running Uboot 2010-10-rc5 as suggested by a email on the board. I am still new to working down to this level of code so any help in understanding this problem is appreciated.

3 3

Linux Virtualization on ODROID-XU4
by Norrathep Rattanavipanon 13 Mar '17

13 Mar '17

Hi, I tried to run Linux on top of seL4 in ODROID-XU4 device. I followed the instruction in https://sel4.systems/Community/Devdays/Workshop2016/ihor-sel4ws2016.pdf. I run with normal u-boot. And I got to the part that it printed out: We used 57776 CSlots (11.02% of our CNode) Done; suspending... Initialising UART driver Initialising UART driver Then it stops there. Any idea of what went wrong here? Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 2

How to implement RM scheduling on seL4
by wang 07 Mar '17

07 Mar '17

Hello, I'm now studying seL4/seL4test and try to implement the RM scheduling on seL4test. I understand how the RM scheduling works, but just don't know how to make it happen on seL4test. So where can I start? In addition, I put the sel4test driver image on my board and run, it shows "206/206 tests passed. All is well in the universe" at the last line. Does it means that the seL4test project runs correctly? Thanks!

3 3

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