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