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/platsupport/timer.h#L165 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
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.