- Devel - lists.sel4.systems

Allocation manager and processes
by Rinat Dobrokhotov 28 Mar '17

28 Mar '17

Hi all, 1. Could you check if my thoughts are right? The allocation manager is global object and there is only one instance for whole system. If I need in creation kernel objects I should create _one_ allocman above some array of memory. 2. I have the first question because I work with processes now. In the root process I create two different processes based on the elf image via allocman. Then I try to manage (suspend, change priority, etc.) process1 by process2. But I can't get process1 object from process2 because both of them belong to root process and belong to root process' memory space. As I understand it, I should copy cap which belongs to process1 to process2, then I will be able to manage them. Could you tell me if I am right? -- Best regards, Rinat Dobrokhotov

2 1

CapDL & RT
by Richard Habeeb 23 Mar '17

23 Mar '17

Hello all, I see that the master branch of CapDL has some support for the RT kernel, but I am having some trouble building it against the current public sel4 RT branch. Which version of the RT kernel does capDL work with? Or, is it still a work in progress? Thanks, Richard -- Richard Habeeb Research Assistant, Computer Science, USF PGP: https://goo.gl/VhmGGu https://habeebr.bitbucket.io/

2 1

sel4 kernel boot problem on i.mx6q board
by shijun zhao 21 Mar '17

21 Mar '17

Hi everyone, I am running sel4 on i.mx6q sabre board. I use the sabre_debug_xml_defconfig config file. However, the image stops at "Jumping to kernel-image entry point..." when I run it on the board. Following is the printed messages: ## Starting application at 0x20000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[20000000..2030081f] ELF-loading image 'kernel' paddr=[80000000..80032fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[80033000..80406fff] vaddr=[10000..3e3fff] virt_entry=203d0 Enabling MMU and paging Jumping to kernel-image entry point... There are some warnings during compilation, all of which are caused by arm-none-eabi/bin/ld. And I see that the sel4 wiki shows how to solve the warnings: *To fix, do make menuconfig visit seL4 Libraries→Build musl C Library and untick libmuslc use precompiled archive then do make clean and attempt to rebuild.* However, there is no *Build musl C library* in my menuconfig, and there are only *libmuslc *and *libsel4muslcsys *options in the seL4 libraries. Can anyone tell me how to solve this problem? Thanks! Best Regards, Shijun

2 4

Help accessing physical address on zynq7000
by Brandon, Jeffrey - 0553 - MITLL 21 Mar '17

21 Mar '17

Hello, I've been getting started with seL4 on the zynq7000 and I am looking for resources on how to read/write physical memory for memory mapped io purposes. If there is a relevant tutorial or manual to reference I haven't come across it yet so I wanted to ask here. Any other guidance as to how to think about and work with capabilities would be useful at this stage. I'm working with a modified version of the sel4test repository. Looking at that I found env.simple (simple_t defined https://github.com/seL4/seL4_libs/blob/a1c031b0885dec4ddf1ee1f8866bcd23dcca6 ac3/libsel4simple/include/simple/simple.h) which seems to contain function pointers for some relevant functions to what I'm trying to do, but I am not entirely sure how to go about using them. What needs to be initialized first and how do I go about that? Any guidance greatly appreciated, Thanks. Jeff Brandon Associate Staff MIT Lincoln Laboratory 05-53 Secure Resilient Systems and Technology Ph: 781.981.9233

2 1

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

15 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 14 Mar '17

14 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 07 Mar '17

07 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 01 Mar '17

01 Mar '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