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
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.systemsmailto: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.
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.systemshttps://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 Rongfei :)
Thanks for giving us the context :)
I am just wondering if you want to measure how long it usually take for a particular API call to take execute (the 'typical' execution time), or how long it can take in the worst case (the worst case execution time).
It sounds like you want to know the worst case execution time for the API calls that you are interested in ?
Yours, Felix
On Tue, Mar 29, 2016 at 5:10 PM, xurongfeik xurongfeik@163.com wrote:
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 listDevel@sel4.systemshttps://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
Hi Felix！
Actually I want to measure how long it usually take for a particular API call to take execute. In other words it means the average execution time. Because we just want to model and simulate the seL4 platform just as in the real environment. Our seL4 model needs to reflect the application results as the same as it runs on real seL4， other than a conservative analysis. Do you know how to get the execution time for the API calls? Because I have met a paper mentioning the execution time can get by user manual, but I can't find the execution time for seL4.
Yours, Xu
At 2016-03-29 19:01:44, "Felix Kam" felixkam42@gmail.com wrote:
Hi Rongfei :)
Thanks for giving us the context :)
I am just wondering if you want to measure how long it usually take for a particular API call to take execute (the 'typical' execution time), or how long it can take in the worst case (the worst case execution time).
It sounds like you want to know the worst case execution time for the API calls that you are interested in ?
Yours, Felix
On Tue, Mar 29, 2016 at 5:10 PM, xurongfeik xurongfeik@163.com wrote: 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.systemshttps://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 -
Thomas Sewell -
xurongfeik