Re: [seL4] Getting timer info from seL4 kernel

On 17 May 2016, at 8:28 am, Gernot Heiser wrote:

On 17 May 2016, at 1:28 , Julien Delange wrote:

...

Now, about the real-time extensions, I do have some questions: 1. Is there any documentation about it? 2. What are the new features? Are they documented? Is there a support with CAmkES? I remembered having seen something like _period and _budget attributes in CAmkES but no documentation. What is the unit (processor tickers, nanoseconds?)? Having documentation and/or examples would be appreciated. 3. Where to grab it, use it and experiment it?

We’ll make our latest RT branch publicly available, probably this week. It comes with an updated manual that describes the mechanisms. But note that it is experimental, and details are likely to change before it is merged into mainline. However, it’s overall very mature, and will start to be merged into mainline fairly soon.

In a nutshell, the new model replaces the time slice with a scheduling context (which is a new cap-protected object). An SC is essentially a pair of period and budget, where a thread is restricted to use no more than its budget every period. If period=budget, you get the old time slice back.

Scheduling contexts have a well-defined semantics of donation, they can be passed over IPC, so you can run a server on the budget of its clients with correct accounting (i.e. the client gets charged for the server time), essentially simulating a migrating threads model. There are other goodies, such as timeout exceptions…

The seL4 manual in the RT branch documents all the new kernel objects, syscalls, and behaviours. You can have a look at the manual in the current RT branch while waiting for the newest version to come out: https://github.com/seL4/seL4/tree/rt/manual We are currently preparing to push out a public version of the CAmkES support for the seL4 RT features. This basically makes the scheduling contexts available to be set and initialised from CAmkES. This will also include some examples that show how to do this in CAmkES. Ihor. ________________________________ 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.