- Devel - lists.sel4.systems

Re: [seL4] [seL4/seL4] Real performance comparisons (#21)
by Gernot Heiser 11 Apr '16

11 Apr '16

On 11 Apr 2016, at 8:09 , fresheneesz <notifications(a)github.com<mailto:notifications@github.com>> wrote: I imagine this isn't the right place for this, but i can't find a better one. The correct one is this (devel(a)sel4.systems<mailto:devel@sel4.systems>) I see the performance comparisons at http://l4hq.org/docs/performance.php are run on all different processors. In its current form, the performance numbers here are completely useless. It would be very informative to have real performance benchmarks where the exact same processor is used for every OS in comparison. Otherwise, what am I supposed to do with those number? You’re right that comparisons across different processors are of limited power, but they aren’t useless either, especially when expressed in cycles (and ideally coupled with an understanding of the underlying hardware, eg the insane pipeline depth and speculation of the Pentium 4). However, given that these are different implementations spanning 20 years (some written in assembler), it isn’t possible to run them on the same hardware. The key observation is that no-one has ever done better on any of those processors. Gernot ________________________________ 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.

1 0

i have some questions about domain and thread
by 김은영 04 Apr '16

04 Apr '16

Hi, all first, I do not speak English well. please answer to me easily. i'm studying seL4 kernel source code. i have some questions. 1. What is domain? i read manual but i don't understand well. I hope that you explain to me in detail about the domain. 2. What is the maximum number of threads that can be created in one domain? 3. Usually there is a function to create a new thread in kernel source code. but i can't find the function in seL4 kernel source code. What is the way to create a new user thread in seL4? also, what is the way to exit user thread in seL4? thanks.

2 1

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 31 Mar '16

31 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 30 Mar '16

30 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 30 Mar '16

30 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 29 Mar '16

29 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