Modifying the root user thread's CSpace
Hello, 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). 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? (I intend to keep the original seL4_CapInitThreadTCB CNode as my level-1 CNode for this experimentation.) Thank you in advance if you can point me to some reference documentation that may cover how to construct the cspace_root_data argument, guidance, or direction you may be able to give. Sincerely, Ben McCart
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
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 ____________________
<
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
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
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
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.
Sorry, I made a mistake with this. I misremembered the way it worked. The value you had originally was correct. - Alwin
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
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
participants (3)
-
Alwin Joshy -
Ben McCart -
Indan Zupancic