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
Hi Norman,
Our typical use cases did not take advantage of the full GPT functionality. We generally found GPTs increased the user-level complexity, increased the lookup time slightly (especially on older ARM platforms with significant branch mispredict costs), for nothing in return (again, for our use cases).
Instead, we ended up using a "level-bit-skip", i.e. bits to ignore in the decode. This results in the actively decoded bits being the least significant ones - which was the structure we generally used, and was most easily understood by programmers.
Using your example the cap address is broken down into |12|X|14|, where X is the 6 bits effectively skipped. In experimental, it would instead be |X|12|14|.
- Kevin
-----Original Message----- From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Norman Feske Sent: Sunday, 3 May 2015 10:33 AM To: devel@sel4.systems Subject: [seL4] CSpace: resolveAddressBits
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
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Hi Kevin,
On 05/04/2015 02:02 AM, Kevin Elphinstone wrote:
Instead, we ended up using a "level-bit-skip", i.e. bits to ignore in the decode. This results in the actively decoded bits being the least significant ones - which was the structure we generally used, and was most easily understood by programmers.
thank you for the clarification. It is good to know the rationale behind it.
Using your example the cap address is broken down into |12|X|14|, where X is the 6 bits effectively skipped. In experimental, it would instead be |X|12|14|.
My intention was to use the 1st-level CNode to segregate the CSpace into 4096 sub spaces with each having a maximum size of 2^20. The sub spaces vary in size. E.g., one will hold the caps for roottask-allocated kernel objects (dimensioned 2^14) whereas another would hold page frame capabilities (dimensioned 2^20). For organizing the roottask sub space, I will use 3 levels of CNodes |12|6|14| where the second level "emulates" the guard for the third level. This works fine.
Best regards Norman
-
Kevin Elphinstone -
Norman Feske