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.