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