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
Devel@sel4.systems
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.