March 2016 - Devel - lists.sel4.systems

IA32 syscall bindings
by Norman Feske 26 Aug '16

26 Aug '16

Dear seL4 developers, first, I'd like to thank you for publishing seL4 under GPL. I am very happy that I can finally get my hands dirty with working with the kernel of your group. :-) Currently, I am taking the first baby steps to bring the Genode OS framework (http://genode.org) to seL4. For reference, I am using the experimental branch. The first smallish issue I stumbled upon stems from the fact that Genode is written in C++. By compiling the seL4 syscall bindings with a C++ compiler, I got the following error: error: inconsistent operand constraints in an ‘asm’ It can be reproduced by putting the following code snippet into a cc file and compiling it with 'g++ -m32 -c' (tested with the Genode tool chain as well as with GCC 4.8.1): typedef enum { seL4_SysDebugPutChar = -9, _enum_pad_seL4_Syscall_ID = (1U << ((sizeof(int)*8) - 1)) } seL4_Syscall_ID; void seL4_DebugPutChar(char c) { asm volatile ( "pushl %%ebp \n" "movl %%esp, %%ecx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebp \n" : : "a" (seL4_SysDebugPutChar), "b" (c) : "%ecx", "%edx", "%esi", "%edi", "memory" ); } When compiling the same code snippet with 'gcc' instead of 'g++', everything is fine. It turns out that the C++ compiler does not like the enum value to be specified as input argument. I found the following ways to circumvent this problem: * Changing the enum value 'SysDebugPutChar' to a positive value, * Removing the definition of '_enum_pad_seL4_Syscall_ID', * Casting 'seL4_SysDebugPutChar' to an integer: : "a" ((int)seL4_SysDebugPutChar), In any case, I seem to have to change the bindings. Do you see a way around it? If not, would you consider one of the solutions above for the seL4 headers? On another note, I noticed that the bindings use the EBX register. Unfortunately, this makes it impossible to compile seL4 userland software as position-independent code (PIC). E.g., when compiling the above code snippet via 'g++ -m32 -fPIC -c', the following error occurs: error: inconsistent operand constraints in an ‘asm’ However, PIC is required in order to use shared libraries. The solution would be to not use EBX to pass arguments to the 'asm' statements, save EBX on the stack prior moving the respective kernel argument to the register, and, of course, restoring it after sysenter returns. Before I start changing the bindings, I'd like to know: is there anyone else working on the same problem? Would you be open to accept a change of the bindings to become PIC compliant on the costs of a few added instructions? Or do you have another suggestion how I should go about it? Best regards Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

4 7

Questions about Kernel Memory Mapping
by Daniel Wang 01 Apr '16

01 Apr '16

Hi all, I’m trying to understand the seL4 kernel source code. I think the memory mapping between physical memory and virtual memory is a key point since it is directly related to how kernel functions and manage badges. I noticed that the kernel turns on the paging very early. Can someone help me or point out some resources how kernel memory is allocated? Especially how during and after the booting what the kernel memory snapshot looks like and things like that. For example, I traced to map_kernel_window() function and even before that there is some pptr to paddr conversion. I would really appreciate the help. Thanks -Dan

3 2

seL4 Documentation/Tutoria
by xurongfeik 31 Mar '16

31 Mar '16

Hi folks Is there any Documentation/Tutorial about execution time for typical invocations of the seL4 system calls? Thanks! -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University

2 1

sel4 build tutorial
by Jorge Alberto Garcia 31 Mar '16

31 Mar '16

Hi folks Is there any Documentation/Tutorial about how to do a build to start testing seL4 ? where can I find the current boards/architectures supported? Thanks!

2 2

Network Stack and Driver
by Norrathep Rattanavipanon 30 Mar '16

30 Mar '16

Hello, My name is Oak and I'm working with Prof. Gene Tsudik for remote attestation project using sel4. I know that you guys are not interested in developing network stack and drivers for sel4. But do you happen to know if anyone else has done some work with network stack and Wi-fi, Bluetooth or ethernet driver in sel4? Regards, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

答复:答复: 答复:Re: About the execution time of seL4 API
by xurongfeik 29 Mar '16

29 Mar '16

裴老师：您好！谢谢您的资料。现在我们学校有两个团队在做这方面的工作：其中我们实验室主要在模型层对seL4微内核进行建模仿真，主要是把微内核基本功能机制建模成为一个基本模型，对User Mode扩展部分以策略模型的方式与基本模型进行编织，从而建立一套在设计早期通过模型仿真验证策略的方法。目前，我们正着手建立一个能准确反映真实seL4微内核运行的模型，但是由于仿真时钟的不准确，我们希望在某一硬件环境上把seL4微内核模型下层的系统调用时间统计出来，通过时间累加计算seL4微内核模型上的应用执行过程。但是目前不知道该如何获取这些系统调用的执行时间，不知道裴老师您那边是否有相关的数据？另外一个团队主要是基于seL4微内核的操作系统开发，主要考虑分区、并发的不确定性。目前主要用于航天的应用中。如果裴老师有相关的研究，非常愿意共同合作！祝好！许荣飞在 2016-03-29 14:39:35，"XilongPei" <pei.xilong(a)kortide.com> 写道： XuRongfei: 我是同济大学电信学院老师裴喜龙，我们从事你说的这个方向好几年了。附件文件是我把seL4的说明书翻译成了中文，下面这个链接是我们做的高可用操作系统的项目工程页面。 http://elastos.org/redmine/projects/rt-elastos这个工程的源码在： https://github.com/elastos/HD-Elastos 我们基于AOP思想做的操作系统（正在开发中），官网：http://elastos.org/project-guide/ 源码开源在github: https://github.com/elastos/ElastosRDK5_0它基于AOP思想，提出一种构件技术CAR，并基于这个构件技术，实现了一… 希望国内做相关工作的人能合作，共同做一些大的工程。同济大学裴喜龙 2016年3月29日星期二发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 xurongfeik 发送时间: 2016年3月29日 14:11 收件人: Thomas Sewell <thomas.sewell(a)nicta.com.au> 抄送:devel@sel4.systems 主题: [seL4] 答复:Re: About the execution time of seL4 API Thank you for your reply！ My name is XuRongfei, and I am a PHD student from China,Beijing. Now I focus on RTOS Modeling and Simulation. As we know, an important principle of microkernel design is the separation of mechanism and policy, it is what enables the construction of arbitrary systems on top of a minimal kernel. This separation of mechanism and policy is similar to AOM(Aspect-Oriented Modeling) and we can model the mechanism and policy separately. The biggest advantage is that analysis and verification of the policy applied in the implementation phase will be advanced to the design stage. As seL4 Microkernel is "the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement". So if we want to construct an RTOS on top of seL4 Microkernel, it is necessary to simulate and analyse the policy model on the microkernel model first. To simulate the seL4 Microkernel model accurately and agree with the real situation, the execution time of seL4 typical API (such as send\receive\notify message and Resume\Suspend\Create thread) for certain platform. So how can we get the execution time of this APIs for certain platform? Is it possible? Thank you very much! At 2016-03-29 11:45:42, "Thomas Sewell" <thomas.sewell(a)nicta.com.au> wrote: Hmm, what do you mean by measuring the time? You can measure the typical execution time of various system calls easily enough by checking the CPU cycle counter. There is an internal "sel4bench" project which is similar to "sel4test" but measures timing information of some system calls. My understanding is that this will be released at some point in the near future. It's also possible to calculate the worst-case execution time of the kernel for some platforms. There's been a lot of research work on this http://ssrg.nicta.com.au/projects/TS/realtime.pml by various people at Data61/NICTA. It's probably possible to replicate for some platform of interest, but it might be quite difficult to do. Cheers, Thomas. On 29/03/16 14:06, xurongfeik wrote: Hello，everyone： When given a specific platform， is it possible to measure the execution time of seL4 API？ Anyone who has the relative data please send it to me， many thanks！！ -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

2 1

About the execution time of seL4 API
by xurongfeik 29 Mar '16

29 Mar '16

Hello，everyone： When given a specific platform， is it possible to measure the execution time of seL4 API？ Anyone who has the relative data please send it to me， many thanks！！ -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University

3 4

Where can I get the information about Linux on seL4
by XilongPei 29 Mar '16

29 Mar '16

Hi Gernot, I found that the footer of http://ssrg.nicta.com.au/ is: Served by Apache on Linux on seL4 Whare can I get more information about Linux on seL4? Xilong Pei Tongji University 2016/3/29

2 1

Status of ARMv8 support for seL4 ?
by karim.allah.ahmed＠gmail.com 28 Mar '16

28 Mar '16

Hello, >From this roadmap [0], I can see that ARMv8 support is underway at the moment. Is this something that's going to be released soon given that the roadmap says Q1-2016 (at least 32-bit) ? [0] https://sel4.systems/Info/Roadmap -- Karim Allah Ahmed.

1 0

Porting Qubes OS to seL4 project
by Paul Vlase 28 Mar '16

28 Mar '16

No answer ... Am I doing something wrong? Beside not have patience. Could anyone tell about the status of the seL4 Qubes port project and who can I get in touch with to talk more about it? On Tue, Mar 22, 2016 at 11:35 PM, Paul Vlase <vlase.paul(a)gmail.com> wrote: > Hello, > > My name is Paul Vlase and I am following a master degree right now. I > am interested in porting the Qubes OS to seL4 project and I saw that > you are working already on it. Is there anything I can help you on > this project? > > Thank you, > Paul Vlase

2 1