Re: [seL4] RT branch questions

On 27 May 2016, at 3:21 , Ihor Kuz UNSW wrote:

The basic model is that every CAmkES thread (unless specified otherwise) has a scheduling context (SC). The above attributes set the parameters of the associated scheduling context. If not explicitly specified then a thread’s SC has default values (10000) for the period and budget. The values are in microseconds.

With regards to the period and budget they match the same attributes in the scheduling contexts as provided by the kernel. See the kernel manual (RT version) for more details. Priority is the same as in previous versions of seL4.

note that if budget=period, you get the old seL4 scheduling behaviour (where period replaces the time slice).

...

Any information about them? How they are supposed to be isolated from each other then?

If you want to know how this can provide temporal isolation, then the answer is that you can use the budget to prevent a high-prio thread from monopolising the CPU. A thread with period T and budget C is guaranteed to consume no more than C/P of the available CPU bandwidth, irrespective of prio. If that’s the highest-prio thread, then (P-C)/P bandwidth is left to other threads. There’ll be a white paper out shortly. 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.