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. 



[0] https://docs.sel4.systems/Tutorials/capabilities.html