Hello Ben.

There's two reasons a supervisor might want to use the double-lookup CSpace 
operations.

One is to manipulate the CSpace of some client process. The supervisor only 
needs a single CNode capability to the top of the client's CSpace, and can then 
name any accessible part of the client's CSpace at any level.

The double-lookup also allows the supervisor to name and manipulate 
intermediate CNodes in its own CSpace, to perform restructuring operations. 
This isn't necessary if the supervisor also keeps copies of the intermediate 
CNode caps in accessible slots at the bottom of the lookup, which is a tradeoff 
you can make.

Finally, I'm surprised you have to shift by odd sizes. That shouldn't be necessary in 
what I think of as the "usual" layout. This layout has all caps reached via a 
full 32-bit lookup and keeps the CNode cap to the root of the CSpace at a fixed address 
in said CSpace. The double-lookup CSpace operations can then be performed on normal slots 
by providing the same CPtr and some other standard arguments. I think that libsel4 
provides standard wrappers for doing this.

Word of warning: I recall this from the design days, but I don't know if there 
are any new technicalities in the implementation that contradict what I've just 
said.

Cheers,
   Thomas.

On 11/12/15 18:47, Ben Karel wrote:
Hi all,

Some capability resolution, such as for fault handling, winds up calling 
resolveAddressBits with n_bits = wordBits, and any remaining bits are ignored. 
In other cases, such as the destination slot for seL4_CNode_Copy, the user 
provides a resolution depth parameter, and the call to resolveAddressBits is 
mediated by lookupSlotForCNodeOp, which fails with a depth mismatch if there 
are any bits remaining.

Individually these seem like reasonable choices, but it leads to code like this:

   seL4_CNode cspace_root = ...; // freshly allocated 256-slot CNode with no 
guard
   seL4_CPtr slot_for_copy = 0x23; // arbitrary slot we know is available
   seL4_CPtr slot_for_tcb = slot_for_copy << 24;

   seL4_CNode_Copy(cspace_root , endpoint_for_copy, 8, ...);
   seL4_TCB_Configure(..., endpoint_for_tcb, ...);

I found it surprising that two different CPtrs are needed to describe the same 
slot! Is there a conceptual-model-explanation that doesn't involve appeal to 
the underlying implementation?

Also: my current understanding is that the depth parameter is only needed to 
disambiguate indirections through CNode-containing slots. What goes wrong if 
the depth mismatch checks are relaxed?





_______________________________________________
Devel mailing list
[email protected]<mailto:[email protected]>
https://sel4.systems/lists/listinfo/devel



________________________________

The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to