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 -- [email protected]
To unsubscribe send an email to [email protected]
_______________________________________________
Devel mailing list -- [email protected]
To unsubscribe send an email to [email protected]
