Hello Ben, I think you have a good understanding of how CSpaces work now. On 2024-11-14 19:12, Ben McCart wrote:
Thank you for the explanation that was helpful. I decided to try and make a two level CSpace with 16 bits of radix for each level, and 32 gaurd bits for the root CNode of all zeros.
If you want to use seL4_CapInitThreadCNode with a two level 16 bits CSpace: - Assert bi->initThreadCNodeSizeBits <= 16. - When copying the seL4_CapInitThreadCNode cap into your new CNode, give it a guard size of 16 - bi->initThreadCNodeSizeBits so it adds up to 16 bits in total. You can also use CONFIG_ROOT_CNODE_SIZE_BITS, it's the same. An alternative to the above is to set KernelRootCNodeSizeBits config option to 16 instead of doing the above. If you do, add an assert it's actually 16 to avoid future pain.
// Link the first cslot in the new root cnode to the original cnode, so that original root cnode CPtrs remain valid. error = seL4_CNode_Copy( cspace_cap, 0, // Destination index in the new Cap table. 16, // Number of bits for the new Cap table. seL4_CapInitThreadCNode, seL4_CapInitThreadCNode, seL4_WordBits, seL4_AllRights); kernel_assert(error == seL4_NoError);
seL4_CNode_Copy can't change the guard, you have to use seL4_CNode_Mint() if you need to change it: assert(bi->initThreadCNodeSizeBits <= 16); seL4_CNode_Mint( cspace_cap, 0, // Destination index in the new Cap table. 16, // Number of bits for the new Cap table. seL4_CapInitThreadCNode, seL4_CapInitThreadCNode, seL4_WordBits, seL4_AllRights, 16 - bi->initThreadCNodeSizeBits); // Zero pad guard to reach 16 bits.
// Set the new cnode as the root for the cspace. seL4_Word cspace_guard = 0x0000000000000020; // Guard of 32 bits, all zeros.
Personally I would write this as just 32, or 0 | 32, because you're only setting the guard size. Greetings, Indan