Hi Julien,
I've answered the questions I can, I know more about seL4 than CAmkES though:
- How the real-time requirements are handled in camkes? For example, how can I specify
that a component is executed periodically every XXX ms. Does the ADL supports that?
Experimental support for real-time, periodic threads will be released in the coming months
for seL4 and CAmkES (we are working on it now). Currently periodic threads can be achieved
by using a timer component which threads communicate with in order to sleep.
- How can we specify the scheduling constraints? Can we have an ARINC653-like scheduling
where every process has a fixed time slice to be executed? Since the behavior of the
system can be deduced from the execution time, allocated a fixed time slice also avoid
some attacks
This will come with the above real-time extensions.
- About scheduling, what are the policies actually supported?
Currently fixed priority round-robin is the only scheduling policy supported. Other
policies can be achieved with a scheduler component.
There is also a domain scheduler which allows threads to be placed in isolated domains
with fixed length domain timeslices.
- How timing is handled? I tried to use nanosleep() from the libc but it seems the
syscall/service is not implemented. I also tried the timer example from the sel4 tutorial
but when compiling, there is an error (the function timer_handle_irq needs an IRQ as a
parameter). Any idea how to fix the example and more information about how time is
handled?
The kernel does not provide access to time, however we have some user level timers
available. The tutorials are currently not up to date, but you can use the function here:
https://github.com/seL4/util_libs/blob/master/libplatsupport/include/platsu…
to get the irq number to handle (with n=0).
- is it possible for the OS to load and launch multiple elf at the same time or other
processes must be manually started?
Manually, but CAmkES + the capDL loader can also do this for you using user level
infrastructure.
- How capabilities and services are associated? From the example hello-2 in the sel4
tutorial, I see that a capability is declared (with vka_alloc_endpoint(&vka,
&ep_object)) but I do not understand how this is associated with the message being
sent between both tasks. In other words, how is it possible to associated a capability
with a service. When sending or receiving a message (for example, by using seL4_SetMR(0,
MSG_DATA);), there is no use of the capability. So, how the kernel can check that the
thread can effectively send a message?
seL4_SetMR just sets a message word in the IPC buffer, but does not perform the send. The
kernel does this check when seL4_Call, seL4_Send or seL4_NBSend are used and the message
will be received by the first thread that waits on the endpoint. For more details please
see the manual.
- Is there any efforts to support standards such as ARINC653 or MILS? (even experimental)
ARINC can be achieved with the domain scheduler in master seL4, however we haven't
actually built user level support for it.
- Is there any significant/big projects that are available online and you would recommend
to learn the OS and its associated libraries?
To get familiar with the code base, you can do the advanced operating systems project:
http://www.cse.unsw.edu.au/~cs9242/15/project/index.shtml
I recommend you use sel4test as a guide for use of our libraries:
https://github.com/seL4/sel4test-manifest
I can't answer the following questions, but I'll point someone who can to them:
- About camkes, what are the thread mapping rules. How a component is transformed into one
(or several) sel4 threads? Is there a mapping 1 component = 1 thread or is it possible to
have multiple threads per component?
- How can I find the code generated by camkes? The idl/adl code is ultimately transformed
into C code and I was wondering where I could see the code.
Cheers,
Anna.
On 26/12/2015 10:14 am, Julien Delange wrote:
Hello,
First of all, thanks for the help you provided previously. After downloading the virtual
machine, everything was fine and I was able to try seL4 and camkes by using the tutorials.
Thanks also for making this documentation available publicly, it definitively helps a lot
to learn the principles of this operating system.
I still do have some questions regarding sel4 and camkes.
- About camkes, what are the thread mapping rules. How a component is transformed into one
(or several) sel4 threads? Is there a mapping 1 component = 1 thread or is it possible to
have multiple threads per component?
- How can I find the code generated by camkes? The idl/adl code is ultimately transformed
into C code and I was wondering where I could see the code.
- How the real-time requirements are handled in camkes? For example, how can I specify
that a component is executed periodically every XXX ms. Does the ADL supports that?
- How can we specify the scheduling constraints? Can we have an ARINC653-like scheduling
where every process has a fixed time slice to be executed? Since the behavior of the
system can be deduced from the execution time, allocated a fixed time slice also avoid
some attacks
- About scheduling, what are the policies actually supported?
- How timing is handled? I tried to use nanosleep() from the libc but it seems the
syscall/service is not implemented. I also tried the timer example from the sel4 tutorial
but when compiling, there is an error (the function timer_handle_irq needs an IRQ as a
parameter). Any idea how to fix the example and more information about how time is
handled?
- is it possible for the OS to load and launch multiple elf at the same time or other
processes must be manually started?
- How capabilities and services are associated? From the example hello-2 in the sel4
tutorial, I see that a capability is declared (with vka_alloc_endpoint(&vka,
&ep_object)) but I do not understand how this is associated with the message being
sent between both tasks. In other words, how is it possible to associated a capability
with a service. When sending or receiving a message (for example, by using seL4_SetMR(0,
MSG_DATA);), there is no use of the capability. So, how the kernel can check that the
thread can effectively send a message?
- Is there any efforts to support standards such as ARINC653 or MILS? (even experimental)
- Is there any significant/big projects that are available online and you would recommend
to learn the OS and its associated libraries?
Hope you do not mind such a list of questions! I really enjoy digging into the OS and it
seems very interesting.
Thanks for any help/comment.
_______________________________________________
Devel mailing list
Devel@sel4.systems<mailto: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.