Hello,
the seL4 kernel constructs the root task's CNode (in kernel/boot.c) by
using the configurable number CONFIG_ROOT_CNODE_SIZE_BITS as size and a
guard value calculated as 32 - CONFIG_ROOT_CNODE_SIZE_BITS. I understand
that it makes the capability name space nicely linear. But on the hand,
doesn't it impede the number of kernel objects addressable by root task?
When using Genode's core as root task on seL4, I will need to maintain a
large number of capabilities to kernel objects, in particular one for
each page managed by the core process. Naturally. I would like to
organize the root task's capability namespace hierarchically, allocating
CNodes depending on the dynamic work load. As far as I understand,
however, root task would have no way to address slots within such
additional CNodes because all address bits are already consumed by the
root CNode indices + guard. For example, how is root task supposed to
specify capabilities that are not contained in the root CNode as
"service" argument to functions like 'seL4_TCB_WriteRegisters'?
One way I see would be to move capabilities back and forth between the
root CNode and other CNodes using 'seL4_CNode_Copy', effectively using
the root CNode as a kind of CNode cache. But this solution seems overly
complicated.
Another way would be to dimension CONFIG_ROOT_CNODE_SIZE_BITS
pessimistically. But introducing such an upper bound a-priory would
somehow contradict with seL4's otherwise nicely dynamic resource management.
Yet another way would be to let root task use a smaller guard value that
leaves enough bits available to be used for second-level or third-level
CNodes. But since that would require a change of the kernel code, I
suspect that this approach is not in line with right seL4 way.
Could you share the reasoning behind the guard-value calculation and
help me to get on the right track? Or would you consider a configurable
guard value for root task as a reasonable feature request?
Cheers
Norman
--
Dr.-Ing. Norman Feske
Genode Labs
http://www.genode-labs.com · http://genode.org
Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
