[seL4] Re: Modifying the root user thread's CSpace

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 Sent: Friday, November 15, 2024 6:12 AM To: Indan Zupancic Cc: 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 ____________________ <> 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