Hi Ben, Could you try setting the guard to 0x8000000000000000 (0x20 << 58). I think the most significant 6 bits of the cspace guard are used for the size and the rest for the value. Could you also try changing the depth of your last untyped_retype to have node_depth = seL4_WordBits - initThreadCNodeSizeBits (assuming the boot CNode also has radix 16). I think the reason for this is that you want to the lookup to be resolved to the 2nd level of the cspace and if you set the depth to the full word size, it will keep going and attempt to resolve a slot inside the second level CNode. I'm still not great at this stuff, so I might be wrong, but you can find an example of bootstrapping an seL4 system to create a two-level CSpace in this example, which you might find helpful: https://github.com/SEL4PROJ/AOS/blob/master/sos/src/bootstrap.c If it's still not working, let me know and I'll try to help more. - Alwin ________________________________ From: Ben McCart <ben@mccart.us> Sent: Friday, November 15, 2024 6:12 AM To: Indan Zupancic <indan@nul.nu> Cc: devel@sel4.systems <devel@sel4.systems> Subject: [seL4] Re: Modifying the root user thread's CSpace Indan, 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. I am still doing something wrong, but it is not clear to me what exactly, as after setting the new CSpace any calls that I try to do end up throwing cap faults. I have shown my code below (with values), do you (or anyone else reading this post) spot anything obvious? (I don't understand why the 'service' argument for seL4_UntypedRetype would cause a cap fault, I thought my changes to CSpace would leave those boot info untyped caps as valid CPtr with the way I set things up.) ________________________________________________________________________________ // seL4_BootInfo.untyped = {start = 382, end = 474} // A 2MiB untyped was created from a larger untyped using cap 474... code not shown. // Create the new cspace root cnode. seL4_Error error = seL4_Untyped_Retype( page1_cap, // service (untyped of 2M, cap value = 474) seL4_CapTableObject, // type 16, // size-bits ... seL4_CapInitThreadCNode, // root 0u, // node-index 0u, // node-depth-bits cspace_cap, // node-offset (value = 475) 1u // number of tables.); ); kernel_assert(error == seL4_NoError); // 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); // Set the new cnode as the root for the cspace. seL4_Word cspace_guard = 0x0000000000000020; // Guard of 32 bits, all zeros. error = seL4_TCB_SetSpace( seL4_CapInitThreadTCB, // root thread TCB cap. seL4_CapNull, // fault_ep cap cspace_cap, // root CNode cap (value = 475) cspace_guard, // guard size & bits. seL4_CapInitThreadVSpace, // root thread V-space. 0u); kernel_assert(error == seL4_NoError); // The following fails with a cap fault. error = seL4_Untyped_Retype( page_u_cap, // service (root untyped of more than 4K from seL4_BootInfo, cap value = 450) seL4_UntypedObject, // type 12, // size-bits ... cspace_cap, // root seL4_CapInitThreadCNode, // node-index seL4_WordBits, // node-depth-bits new_cap, // node-offset (value = 476) 1u // number of untyped.); ); kernel_assert(error == seL4_NoError); ____________________ Result in Terminal ____________________ <<seL4(CPU 0) [handleInvocation/386 T0xffffff801fe08400 "rootserver" @40131d]: Invocation of invalid cap #450.>> Caught cap fault in send phase at address 0 while trying to handle: cap fault in send phase at address 0x1c2 in thread 0xffffff801fe08400 "rootserver" at address 0x40e893 With stack: 0x566078: 0x40eb2e 0x566080: 0x0 0x566088: 0x0 0x566090: 0x2 0x566098: 0xc 0x5660a0: 0x0 0x5660a8: 0x1c2 0x5660b0: 0x1dc 0x5660b8: 0x0 0x5660c0: 0x0 0x5660c8: 0xc 0x5660d0: 0x0 0x5660d8: 0x408d61 0x5660e0: 0x1086 0x5660e8: 0x566150 0x5660f0: 0x5661c0 On 11/11/2024 5:22 AM, Indan Zupancic wrote:

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 _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

Hello Alwin, Things would have been simpler if root had to be the destination CNode so that node_index would be an actual CSlot index. But alas, that's not how it works, node_index is just a relative CSpace path. On 2024-11-14 20:30, Alwin Joshy via Devel wrote:

Could you also try changing the depth of your last untyped_retype to have node_depth = seL4_WordBits - initThreadCNodeSizeBits (assuming the boot CNode also has radix 16). I think the reason for this is that you want to the lookup to be resolved to the 2nd level of the cspace and if you set the depth to the full word size, it will keep going and attempt to resolve a slot inside the second level CNode.

Actually, it's correct: seL4_CapInitThreadCNode is a CNode path that resolves to a slot in the initial CSpace, and to reach it you do need to resolve all 64 bits. You're mixing up caps with the object they point to. He may have made the 2-level layout compatible with the original CSpace, but that also makes it more confusing in some ways. Basically there are multiple paths to reach the destination slot: new_cspace -> init_cspace[cspace_cap] -> new_cspace -> init_cspace[dest] new_cspace -> init_cspace[seL4_CapInitThreadCNode] -> init_cspace[dest] The destination slot can be reached by either using cspace_cap as root or seL4_CapInitThreadCNode as root in the retype call. This should also work and is simpler, as it doesn't depend on the CSpace layout: seL4_Untyped_Retype( page_u_cap, // service seL4_UntypedObject, // type 12, // size-bits ... seL4_CapInitThreadCNode, // root cap 0, // node-index 0, // node-depth-bits, nothing left to resolve. new_cap, // node-offset (value = 476) 1u // number of untyped.); ); That's what the AOS code also does. To do what I think you had in mind: seL4_Untyped_Retype( page_u_cap, // service seL4_UntypedObject, // type 12, // size-bits ... cspace_cap, // root cap 0, // node-index, same as for the seL4_CNode_Copy/Mint call. 32 - initThreadCNodeSizeBits, // node-depth-bits, all remaining bits except for the CNode slots. new_cap, // node-offset (value = 476) 1u // number of untyped.); ); Note that if you use the root CSpace cap you don't use "seL4_CapInitThreadCNode" anywhere. Keep in mind that the guard size/value is part of the reference to a CNode. You have to compensate for it in node-depth-bits when addressing init_cspace via cspace_cap (I think...), but you don't have to do same for the SetSpace guard as that's already done when resolving the root CNode, that's why it's 32 and not 64. At this point my brain is mush and I'm not sure about anything any more. Like I said, CSpace management is one of the harder parts of using seL4. Greetings, Indan