I am attempting to prototype an seL4 based system that ideally will have multiple threads, each with their own CSpaces which are each a tree e.g. not rooted in the initial cnode. My strategy here is to 1. chain new cnodes off of the initial cnode in the initial thread, and 2. Create a new thread TCB etc., revoke the initial cnode caps and set the new cnode cap as it’s own cnode root in that new thread. I have run into some issues at step 1 and am writing to ask if this is a viable strategy.
Perhaps I am misunderstanding something but chaining in this way does not seem possible if all 32 bits are to be resolved in searching the initial cnode, so I am not certain if this strategy will work. Is it possible to configure the initial cnode guard to be something other than 32 bits? I have searched through the config of the kernel and cannot find some easily changed parameter for compile time, and for runtime I have tried to use the TCB_SetSpace and TCB_Configure on the initial thread to change the guard but this has lead to other problems. If I set it to something like 16, does this mean that all of the slot indices in the bootinfo struct are no longer valid as being set at 0x0, 0x1, etc and now will be at half word indices? It is very unclear to me from the documentation how this works but perhaps I am missing something. Setting it to something like 4 leads to an explicit TCB illegal operation and something larger like 19 returns seL4_Error 3 illegal op when I try to create new cnodes via untyped_retype from the init cnode.
Is there something obvious that I am missing? I wonder if this is even possible—having cnodes not rooted in the initial cnode. Or if it is possible, is there some other mechanism to create a new cnode that is not rooted in the initial cnode? It is also probably important to note that due to constraints I am not able to use any of the nice sel4_libs provided to help with this.
Thanks very much in advance for any help.
Alexandra Clifford, MS
05-53 Secure Resilient Systems and Technology
MIT Lincoln Laboratory
244 Wood st., Lexington MA 02421
Email: Alexandra.Clifford@ll.mit.edu
Hi Alexandra,
I am attempting to prototype an seL4 based system that ideally will have multiple threads, each with their own CSpaces which are each > a tree e.g. not rooted in the initial cnode.
Yes, this is possible. I'm curious as to why you want such a structure? Will the threads also have different virtual address spaces?
My strategy here is to 1. chain new cnodes off of the initial cnode in the initial thread, and 2. Create a new thread TCB etc., revoke the ?> initial cnode caps and set the new cnode cap as it’s own cnode root in that new thread.
The revoke step reads wrong to me. If you create new caps from an initial cap, then call revoke on those initial caps, you'll be deleting all of the caps you have just created.
Is it possible to configure the initial cnode guard to be something other than 32 bits?
Yes. The general rule is that the guard size needs to be seL4_WordBits - the amount of bits you want to resolve in the cspace. If I have a cnode that has 2^12 slots, so takes 12 bits to address, then the guard needs to be seL4_WordBits - 12. This is because invocations done by that TCB lookup caps at a depth of seL4_WordBits from the root cnode set in that TCB.
I wonder if this is even possible—having cnodes not rooted in the initial cnode.
This is possible.
Or if it is possible, is there some other mechanism to create a new cnode that is not rooted in the initial cnode?
The steps to do this are:
1. Create a new cnode in a slot in the initial cnode 2. set the Cspace root of the new TCB to the created cnode (by referring to the cap in the initial cnode) 3. Set the guard size of that TCB to seL4_WordBits - the address it takes to address the cnode.
If you want to place other capabilities into the new cnode from the initial thread, you will need to use a depth equivalent to of address bits for the initial cnode + address bits of the new cnode.
Good luck! Please ask further questions if this doesn't make sense. It's on my list to write a more in-depth capability addressing tutorial than the existing one [0]
Cheers
Anna.
-
Clifford, Alexandra - 0553 - MITLL -
Lyons, Anna (Data61, Kensington NSW)