Hello Ben, Welcome to one of the most tricky parts of using seL4, CSpace management! On 2024-11-08 16:58, Ben McCart wrote:

I read the manual for v12.0 chapters 1-3, and 10.  I have been attempting to experiment with CSpaces for the user space root thread.  I am trying to modify the CSpace to support multiple CNode levels by changing the guard from all zero bits above the radix (16 bits of radix on PC99 x64), to support multiple CNode levels.  I have been using seL4_TCB_SetSpace to modify the CSpace for seL4_CapInitThreadTCB.  The result is seL4_NoError and once I make this call the previously working capabilities tutorial quits working as expected. (Calls taking the original seL4_CapInitThreadTCB value are now returning seL4_InvalidCapability). 

Assuming you only changed the guard value and kept the size the same, from this point on you should add this guard value to the cap defines when using them, e.g. (guard << initThreadCNodeSizeBits) | seL4_CapInitThreadTCB If you create a define for this, you can use it after the CSpace change: #define CSPACE_GUARD1 0x1234 #define CSPACE_SIZE1 initThreadCNodeSizeBits #define G(cap) ((CSPACE_GUARD1 << CSPACE_SIZE1) | (cap)) And then you can use G(seL4_CapInitThreadTCB) after the seL4_TCB_SetSpace call to access the original cap. (Remember, CSpace paths are resolved from high to low bits.)

I have studied chapter three of the manual and I think I understand how the CSpace addressing works in depth.  What I can't seem to figure out is how to construct a cspace_root_data argument for the call to seL4_TCB_SetSpace for the number of guard bits and the guard values I want to use.  For example, if I wanted two levels each with a 4 bit guard and a 16 bit radix how would I construct cspace_root_data argument for a gaurd value of 0x0?   And for a gaurd value of 0xF?

The manual doesn't document clearly what cspace_root_data should be. It should be set to: (guard << seL4_GuardSizeBits) | guard_size_in_bits Or you can use seL4_CNode_CapData_new(seL4_Uint64 guard, seL4_Uint64 guardSize) instead. For a 1-level CSpace guard bits + radix should add up to 64 for a 64-bit platform. For multilevel CSpace they all should add up to 64 together. 2 * (4 + 16) = 40 bits, it needs to be 64. You can zero-pad the first guard to make it fit (so increasing the guard size to 28): 0x000000GnnnnGmmmm Or go for a 50-50 split with guard sizes of 16 for both: 0x000Gnnnn000Gmmmm (The 0's above are part of the guard values.)

(I intend to keep the original seL4_CapInitThreadTCB CNode as my level-1 CNode for this experimentation.)

If you want the original caps to be usable, you need to make the initial CNode the last level CNode (a leaf in the CNode tree structure). Only the CNode methods can handle caps at different levens than full path resolution, because they get the lookup depth as an extra parameter. All other methods will try to resolve the full 64 cap bits and give an error if they can't resolve all of them. Lastly, guard bits are not a property of the CNode, but a part of the reference to a CNode (inside a CNode cap). This means CNodes can be shared and used by different tasks with different guards and CSpace layouts. Most people using seL4 for real systems with more complexity will probably end up using a 2-level CSpace. Good luck, Indan