Hello,
I am trying to construct a custom CSpace for my root task using seL4's
guarded page-table concept.
At the 1st level, there is a CNode with a radix of 12 and a guard of 0.
At the 2nd level, there is a CNode with a radix of 14 and a guard of 6.
After copying the initial capabilities to the 2nd-level CNode, switching
to this CSpace, and invoking a system call that takes a capability as
argument (seL4_TCB_Suspend), the kernel tells me:
<<seL4 [decodeInvocation/609 Te3ffa880 @10245c2]: Attempted to invoke
a null cap #1.>>
The problem seems to be a failed 'lookupCapAndSlot', which internally
calls 'resolveAddressBits':
https://github.com/seL4/seL4/blob/experimental/src/kernel/cspace.c#L138
While inspecting the function, it does not appeared to me why it does
not consider any guard bits within the while loop. The 'levelBits'
variable is simply set to 'radixBits'. Interestingly, the same function
in the master branch looks different. Here, the 'guardBits' are taken
into account, which is consistent with the documentation.
I wonder, why differs the experimental branch to the master branch in
this respect?
Is there a way to construct the scenario above with the experimental
branch? The only work-around I see is to allocate an intermediate CNode
with a size of 2^6 that sits between the 1st and 2nd level. Or is there
a better way?
Best regards
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
