裴老师： 您好！谢谢您的资料。 现在我们学校有两个团队在做这方面的工作： 其中我们实验室主要在模型层对seL4微内核进行建模仿真，主要是把微内核基本功能机制建模成为一个基本模型，对User Mode扩展部分以策略模型的方式与基本模型进行编织，从而建立一套在设计早期通过模型仿真验证策略的方法。 目前，我们正着手建立一个能准确反映真实seL4微内核运行的模型，但是由于仿真时钟的不准确，我们希望在某一硬件环境上把seL4微内核模型下层的系统调用时间统计出来，通过时间累加计算seL4微内核模型上的应用执行过程。但是目前不知道该如何获取这些系统调用的执行时间，不知道裴老师您那边是否有相关的数据？ 另外一个团队主要是基于seL4微内核的操作系统开发，主要考虑分区、并发的不确定性。目前主要用于航天的应用中。如果裴老师有相关的研究，非常愿意共同合作！
祝好！ 许荣飞
在 2016-03-29 14:39:35，"XilongPei" pei.xilong@kortide.com 写道：
XuRongfei:
我是同济大学电信学院老师裴喜龙，我们从事你说的这个方向好几年了。
附件文件是我把seL4的说明书翻译成了中文，下面这个链接是我们做的高可用操作系统的项目工程页面。
http://elastos.org/redmine/projects/rt-elastos%E8%BF%99%E4%B8%AA%E5%B7%A5%E7... https://github.com/elastos/HD-Elastos
我们基于AOP思想做的操作系统（正在开发中），官网：http://elastos.org/project-guide/ 源码开源在github: https://github.com/elastos/ElastosRDK5_0%E5%AE%83%E5%9F%BA%E4%BA%8EAOP%E6%80...
希望国内做相关工作的人能合作，共同做一些大的工程。
同济大学 裴喜龙
2016年3月29日星期二
发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 xurongfeik 发送时间: 2016年3月29日 14:11 收件人: Thomas Sewell thomas.sewell@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@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@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.
Hi Xu (My apology if that's not your given name) :)
If you want to measure the typical / average execution time of the various seL4 API calls, I think following what Thomas said would be a really good starting point:
" 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 sounds like you have been trying to access the CPU cycle counters ? ("但是由于仿真时钟的不准确，我们希望在某一硬件环境上把seL4微内核模型下层的系统调用时间统计出来， 通过时间累加计算seL4微内核模型上的应用执行过程。")
If that's the case, you want to pick a processor of interest, get their hardware manual and figure out how to setup and use the cycle counter. If you are using one that's well-supported by seL4 (the sabre lite's processor for example), some of us may have existing code for it.
You also said your group is looking into using this Elastos, which is based on seL4, in avionics ("目前主要用于航天的应用中"), if that's the case you may want to consider the worst case execution time.
Cheers :) Felix
On Wed, Mar 30, 2016 at 12:32 AM, xurongfeik xurongfeik@163.com wrote:
裴老师： 您好！谢谢您的资料。 现在我们学校有两个团队在做这方面的工作： 其中我们实验室主要在模型层对seL4微内核进行建模仿真，主要是把微内核基本功能机制建模成为一个基本模型，对User Mode扩展部分以策略模型的方式与基本模型进行编织，从而建立一套在设计早期通过模型仿真验证策略的方法。
目前，我们正着手建立一个能准确反映真实seL4微内核运行的模型，但是由于仿真时钟的不准确，我们希望在某一硬件环境上把seL4微内核模型下层的系统调用时间统计出来，通过时间累加计算seL4微内核模型上的应用执行过程。但是目前不知道该如何获取这些系统调用的执行时间，不知道裴老师您那边是否有相关的数据？ 另外一个团队主要是基于seL4微内核的操作系统开发，主要考虑分区、并发的不确定性。目前主要用于航天的应用中。如果裴老师有相关的研究，非常愿意共同合作！
祝好！ 许荣飞
在 2016-03-29 14:39:35，"XilongPei" pei.xilong@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，并基于这个构件技术，实现 了一个与Android兼容的操作系统，也是希望把这个基于Linux内核的OS精减，跑在seL4 https://github.com/elastos/ElastosRDK5_0%20也是希望把这个基于Linux内核的精减成跑在seL4 内核上。
希望国内做相关工作的人能合作，共同做一些大的工程。 同济大学 裴喜龙 2016年3月29日星期二*发件人:* Devel [mailto:devel-bounces@sel4.systems] *代表 *xurongfeik *发送时间:* 2016年3月29日 14:11 *收件人:* Thomas Sewell thomas.sewell@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@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@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.
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-
Felix Kam -
xurongfeik