November 2018 - Devel - lists.sel4.systems

Passing Network Resource to Linux VM in TK1-SOM
by Daniel Wang 06 Nov '18

06 Nov '18

Hi all, I got a question, how can I pass the network communication to Linux virtual machine? Following the work of seL4-ARM-VMM with TK1-SOM board, i run seL4 as the microvisor that hosts the buildroot Linux as a user-land process, I was able to mount the MMC storage in the virtual machine, but I cannot get the NIC works. I’m wondering has anyone tried it that can give me some hint? Best Regards -Daniel Wang

2 2

run docker on sel4
by Jia He 06 Nov '18

06 Nov '18

Hi all I am new comer to sel4 community. I knew a little bit virtualisation infrastructe(kvm/qemu), but I know little about sel4/docker. I am investigating the proper implemenatation for running docker on sel4 on arm64. There might several ways I can figure out.Any suggestions are welcome :-) 1. run linux on sel4 vmm (camkes_vm) and run docker on linux. This might be the easiest way. It might have worked well on X86 2. porting l4linux to sel4. Don't know whether it is feasible? 3. run docker as sel4 service without linux. On this way, golang and its library should be ported to sel4. Some missed syscalls which are needed by docker should be implemenated. Is there any other ways or anything else to make the implatation more feasible? --- Cheers, Justin

3 2

seL4 IPC and SMP question.
by 송대영 05 Nov '18

05 Nov '18

HI, I have a question about IPC and SMP. I ran sel4bench on sabre lite(i.mx6, arm v7). 1. I want to confirm performance difference between Lazy Scheduling and Beno Scheduling. Can I configure scheduler? 2. Can you explain the difference when thread state is "ThreadState_Running" and "ThreadState_Restart"? 3. I tried "SMP Benchmark" but I can't understand what this benchmark exactly means. What "Cycles" means in this benchmark? smp : This is an intra-core ipc round-trip benchmark to check overhead of the kernel synchronization on ipc throughput. 4. I try to measure IPC performance with SMP is on. I used "seL4_TCB_SetAffinity" function so server executed in Core1 and client executed Core2. But performance results are too excessive. seL4_Call(same vspace, ipc length is 0)' result is 129331186 cycles. Are these results are available?

3 2