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?