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.
