I am currently trying the RT branch and have some questions:
1. What emulator to use in order to try the examples? I am trying to use x86 with qemu but it seems that it does not work. I got the following trace at execution
Starting node #0 APIC: unsupported platform, TSC-deadline mode is not supported seL4 called fail at /home/sel4/camkes-sc-tests/kernel/src/arch/x86/kernel/boot_sys.c:451 in function boot_sys, saying "boot_sys failed for some reason :(
So, is there an emulator (for any supported platform) to try it?
2. In the RT-camkes extensions, I have the following new attributes: _period _budget _priority
What is the semantics of these attributes? Any information about them? How they are supposed to be isolated from each other then? How to define the scheduling plan for the system then? Also, how these attributes apply to all thread: a thread is created for each interface of the component, so, how can we then define the priority/budget of each thread? Do these attributes apply to all the components of the thread?
Thanks for any help/clarification.
Julien.
assembly { composition { component Client client1; component Client client2; } configuration { client1._priority = 100; client1._period = 10000; client1._budget = 7500; client2._priority = 50; client2._period = 10000; client2._budget = 7500; } }
On 27 May 2016, at 1:16 am, Julien Delange julien.delange@gmail.com wrote:
- In the RT-camkes extensions, I have the following new attributes:
_period _budget _priority
What is the semantics of these attributes?
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.
Any information about them? How they are supposed to be isolated from each other then?
I’m not sure what you mean by isolated. Can you elaborate?
How to define the scheduling plan for the system then? Also, how these attributes apply to all thread: a thread is created for each interface of the component, so, how can we then define the priority/budget of each thread? Do these attributes apply to all the components of the thread?
You set these attributes per thread. The threads are either the control thread (<component>._period, etc) or a thread per interface (<component>.<interface name>_period, etc.)
Hope this helps a bit.
Ihor.
-- Dr. Ihor Kuz Senior Research Engineer | Trustworthy Systems | DATA61 | CSIRO Conjoint Senior Lecturer | CSE | UNSW E ihor.kuz@nicta.com.au T + 61 2 8306 0582 Locked Bag 6016, UNSW, Sydney NSW 1466, Australia www.data61.csiro.au
CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61
________________________________
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.
On 27 May 2016, at 3:21 , Ihor Kuz UNSW ihor.kuz@nicta.com.au 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.
That helps a lot. About the isolation, let me explain. In approaches like ARINC653 (the OS used in the avionics industry) or MILS (which is more in a research stage), each partition gets a fixed amount of time. To clarify, let's assume that a partition is a thread for seL4.
By isolation, I then mean that the scheduler repeats the same static schedule. There is a schedule of all tasks that is repeated every XXX ms (XXX being what we call the major frame). Nothing can preempt this. Such a schedule is done for safety (every task has the time to be executed) and security (nobody can infer any information based on the task execution time).
I need to read more the manual of the RT branch. I will do that.
Also, any information about how to try/test it? How do you guys test the RT extensions? What emulator are you using for development purposes?
Thanks!
Julien.
On Thu, May 26, 2016 at 1:21 PM, Ihor Kuz UNSW ihor.kuz@nicta.com.au wrote:
On 27 May 2016, at 1:16 am, Julien Delange julien.delange@gmail.com
wrote:
- In the RT-camkes extensions, I have the following new attributes:
_period _budget _priority
What is the semantics of these attributes?
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.
Any information about them? How they are supposed to be isolated from
each other then?
I’m not sure what you mean by isolated. Can you elaborate?
How to define the scheduling plan for the system then? Also, how these
attributes apply to all thread: a thread is created for each interface of the component, so, how can we then define the priority/budget of each thread? Do these attributes apply to all the components of the thread?
You set these attributes per thread. The threads are either the control thread (<component>._period, etc) or a thread per interface (<component>.<interface name>_period, etc.)
Hope this helps a bit.
Ihor.
-- Dr. Ihor Kuz Senior Research Engineer | Trustworthy Systems | DATA61 | CSIRO Conjoint Senior Lecturer | CSE | UNSW E ihor.kuz@nicta.com.au T + 61 2 8306 0582 Locked Bag 6016, UNSW, Sydney NSW 1466, Australia www.data61.csiro.au
CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61
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.
On 27 May 2016, at 3:55 , Julien Delange <julien.delange@gmail.commailto:julien.delange@gmail.com> wrote:
Also, any information about how to try/test it? How do you guys test the RT extensions? What emulator are you using for development purposes?
The white paper should answer this. Hold tight for a week…
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.
On 27 May 2016, at 1:16 am, Julien Delange julien.delange@gmail.com wrote:
I am currently trying the RT branch and have some questions:
- What emulator to use in order to try the examples? I am trying to use x86 with qemu but it seems that it does not work. I got the following trace at execution
Starting node #0 APIC: unsupported platform, TSC-deadline mode is not supported seL4 called fail at /home/sel4/camkes-sc-tests/kernel/src/arch/x86/kernel/boot_sys.c:451 in function boot_sys, saying "boot_sys failed for some reason :(
So, is there an emulator (for any supported platform) to try it?
So far the RT kernel only works on actual hardware.
Emulators don’t have accurate timing, and so it hasn’t been interesting for us to make it work on them. Of course for development, using an emulator would be useful, so it’s in our plan to add qemu support, but not a top priority at the moment. Doing so would basically require adding an appropriate kernel driver for the timer provided by the emulator.
Ihor
-- Dr. Ihor Kuz Senior Research Engineer | Trustworthy Systems | DATA61 | CSIRO Conjoint Senior Lecturer | CSE | UNSW E ihor.kuz@nicta.com.au T + 61 2 8306 0582 Locked Bag 6016, UNSW, Sydney NSW 1466, Australia www.data61.csiro.au
CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61
________________________________
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.
Thanks all! Is it possible to send the white paper on this mailing-list once it is done?
Reading at the manual, there are still some unclear behavior: how the signals are managed (e.g. what happens when issuing a seL4_Wait/seL4_Signal() between threads having different criticality which then raise the question of priority inversion and impact on budgets), how one can design a fixed timelime schedule with several timeslices per threads (as in ARINC653/MILS kernels).
Anyway, I will wait the white paper, it will probably address most (if not all) these questions!
Julien.
On Thu, May 26, 2016 at 2:08 PM, Ihor Kuz UNSW ihor.kuz@nicta.com.au wrote:
On 27 May 2016, at 1:16 am, Julien Delange julien.delange@gmail.com
wrote:
I am currently trying the RT branch and have some questions:
- What emulator to use in order to try the examples? I am trying to use
x86 with qemu but it seems that it does not work. I got the following trace at execution
Starting node #0 APIC: unsupported platform, TSC-deadline mode is not supported seL4 called fail at
/home/sel4/camkes-sc-tests/kernel/src/arch/x86/kernel/boot_sys.c:451 in function boot_sys, saying "boot_sys failed for some reason :(
So, is there an emulator (for any supported platform) to try it?
So far the RT kernel only works on actual hardware.
Emulators don’t have accurate timing, and so it hasn’t been interesting for us to make it work on them. Of course for development, using an emulator would be useful, so it’s in our plan to add qemu support, but not a top priority at the moment. Doing so would basically require adding an appropriate kernel driver for the timer provided by the emulator.
Ihor
-- Dr. Ihor Kuz Senior Research Engineer | Trustworthy Systems | DATA61 | CSIRO Conjoint Senior Lecturer | CSE | UNSW E ihor.kuz@nicta.com.au T + 61 2 8306 0582 Locked Bag 6016, UNSW, Sydney NSW 1466, Australia www.data61.csiro.au
CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61
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.
-
Gernot Heiser -
Ihor Kuz UNSW -
Julien Delange