Hi, I am using Genode with the seL4 backend for my research and have questions about some of the core's services.
Address Space: --------------------
1. Referring to section 3.4.4 from the Genode foundation's book. I am not sure I follow how using a different RM for the stack segment helps us provide buffers in between stacks of different threads in a PD.
2. A PD is defined as Address Space and CSpace. I wondered if it is possible to have multiple address spaces inside a PD. The RM for each of these different Address spaces would still be separate capabilities in the singular CSpace for that PD. This way, a thread can potentially jump across different address spaces like [1, 2]. Or multiple threads can have slightly different address spaces.
3. Where am I going with this? I am trying to implement a new type of thread. In this thread(let's call it thread-stack), each thread's stack will be completely isolated from the other threads. That is, threads will not have access to each other's stacks. They will still share the code-section, library, and heap sections. This is a toy idea, so I can get my hand dirty with the Genode basics. I think everything I need to implement is already there in Genode but wanted to get your opinion.
4. Are they any helper functions to clone an entire address space? Replicate the page table hierarchy with the same underlying page frames.
Scheduling: ---------------
Since scheduling is done inside the kernel in seL4, I think we might be limited to the options exposed by the kernel, but I still wanted to run it by you guys to see if I am missing anything.
1. Using the notion of Affinity, I can restrict a thread to run on a particular CPU, but is there a way to restrict other threads from running on a given CPU. I am exploring isolating two threads by ensuring that they run on separate cores. 2. Is there a way to restrict the time slices given to a particular thread. I am thinking of something like cgroups. I see that seL4 has the MCS kernel, which shares some of the motivations. But I think Genode does not support the MCS sel4 kernel.
Debugging Capability Spaces: ---------------------------------------
1. Is the CSpace for a PD the same as CSpace in seL4, or is there a different notion of Cspace in Genode? 2. Is there an easy way to print the entire CSpace for debugging purposes?
Thanks a lot.
Sid sid-agrawal.ca
[1] Light-Weight Contexts: An OS Abstraction for Safety and Performance | USENIX [2] SpaceJMP: Programming with Multiple Virtual Address Space | ACM SIGPLAN