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.