Questions about Address Space, Scheduling and CSpace

[Sid Agrawal]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.genode.org/pipermail/users/attachments/20220107/c8823418/attachment-0001.htm>