Thank you for the feedback, Thomas. I understand the utility of the double-lookup design in general -- it's an elegant solution for the problem at hand! The part I'm confused by is specifically why capability resolution depth mismatches are necessary.

To elaborate on what's going on with the example I showed, and why the shift is there:

seL4_TCB_Configure does not, itself, do any resolution on the fault endpoint cap it is provided. It simply stores the cap for later use. When a fault occurs in the configured thread, seL4 resolves the cap, at a depth of 32 (wordSize) bits, relative to the configured root CSpace for the thread. With the slot offset in the high bits of slot_for_tcb, resolution will find the copied endpoint and stop.

But seL4_CNode_Copy will fail with a capability resolution depth mismatch if we attempt to copy with depth 32, because resolution will stop with 24 extra bits left over. So I passed depth=8 for the copy call, because that's the radix of the CNode we're copying into, and it has no child slots to recurse into. That means that the slot offset should be in the low 8 bits of slot_for_copy.

Things seem like they would be easier/more flexible if the capability resolution depth mismatches weren't checked for. Then a slot in a node could be transparently expanded (at least, transparent in the common case). So: start with an empty 256-slot CNode; the last slot has canonical address 0xFF000000. Allocate a child 256-slot CNode, and rotate it into the last slot; now the canonical address 0xFF000000 refers to the first slot of the child, and 0xFF01... through 0xFFFF... are available. Currently this sort of transparent upgrade doesn't work because the slots must be distinguished based on their depth.

Having thought about this scheme a little more, the primary downside I can see is that depending on the starting node, an expansion can change the result of resolution. Example: with four radix-8 CNodes organized akin to a linked list, A->B->C->D, the address 0 resolves to the first slot of D regardless of whether resolution starts from A or B. But expand the 0'th slot of D to point to E, and now resolution from B will return E[0] but resolution from A stops at D[0]. Still, since depths are still available, a careful client can use them to ensure stable address resolution.

So it seems to me, naively, that removing the depth check would make CSpace management simpler for clients that use CSpaces in simple/stylized ways, and would not impede sophisticated clients from using CSpaces in arbitrary ways. Am I missing some other fatal flaw?

On Sun, Dec 13, 2015 at 11:21 PM, Thomas Sewell <thomas.sewell@nicta.com.au> wrote:

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.
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel