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