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