Confusing parameter name index in CNode and Untyped object invocations

[kent-mcleod]

Context: Invocations that need to address CNodes use a different addressing method than just a seL4_CPtr. They need:

• a seL4_CPtr to a CNode cap that selects which CNode object to start the lookup from,
• a seL4_Word of address/path information to use in the lookup.
• a seL4_Word of the number of bits to resolve in the lookup, the "depth".

The API documentation names the second parameter (with the address/path information) index or node_index. I find this name makes it easy to confuse the parameter as being a CNode object index instead of an address/path of multiple CNode indexes.

Another thing that contributes to the confusion is that the index is almost a seL4_CPtr and is treated the same if the depth argument is WORD_BITS, but for every bit less you want to resolve, the index argument needs to get right shifted by that amount. However, elsewhere you can use a seL4_CPtr to perform an invocation on a non-CNode object located at a depth less than WORD_BITS and you aren't supposed to right shift by the difference.

A better name would be something like address or slot_address.

[kent-mcleod]

Another reason why it's non-intuitive is because the way page-table addressing is handled in the API is the invocation takes an absolute virtual-address and doesn't require the unused bits to be >> shifted.

[lsf37]

I agree index is confusing I was never quite happy with the name either.

Slightly worried about slot_address, since slot is used a lot in the verification, and the address of a slot there would be the kernel virtual address of the CNode + the offset into the CNode, so quite different to the lookup (it's basically the result of a lookup).

Maybe cap_address or just address in a cap context would be fine.

[kent-mcleod]

Maybe we could look at renaming both index and depth to more closely relate to each other. Essentially both arguments are part of the same variable:

struct cnode_path {
  seL4_Word path;  // variable length CNode path
  seL4_Word pathLength; // length of path (number of bits) 
};

[kent-mcleod]

Actually, this comment was wrong: #566 (comment).
Normal seL4_CPtr lookups use lookupSlot in the kernel which calls resolveAddressBits() and is successful even if bitsRemaining != 0 in the lookup result. Lookups for CNode invocations use lookupSlotForCNodeOp which calls resolveAddressBits() but actually checks that bitsRemaining == 0 so won't allow depth=seL4_WordBits and an index that doesn't take the full depth to resolve a cap.

[bennoleslie]

Context: Invocations that need to address CNodes use a different addressing method than just a seL4_CPtr. They need:

• a seL4_CPtr to a CNode cap that selects which CNode object to start the lookup from,
• a seL4_Word of address/path information to use in the lookup.
• a seL4_Word of the number of bits to resolve in the lookup, the "depth".

I am so glad I'm not the only one that finds this confusing!

[bennoleslie]

Just brainstorming some ideas here. I'm not necessarily strongly in favour of any of them, but might inspire others.

1: Perhaps we should have "CapAddress" and "CNodeAddress". I believe it is only when addressing CNodes that you need the additional 'depth' argument.

2: While 'depth' makes sense because it is a tree, I feel that the parameter you are passing represents the number of bits / length of the address that is being decoded. And actually depth isn't great because a node may be three levels deep, but that isn't the thing you pass tin the 'depth' argument.

3: The manual uses CPTR in some places and CPtr in other. We should be consistent. (Assuming the outcome of this issue is updating docs).

4: I find the statement in 3.3.2 that "A capability address is stored in a CPointer (abbreviated CPTR), which is an unsigned integer variable". It seems to imply some difference between a capability address and a CPointer. Really there isn't one. It previously describes "a capability address is simply an integer". The only difference is that a CPointer is a specific storage location in a user's program. But this confuses things (in my opinion).

5: Of course a capability address actually refers to a "slot" in a CNode. That slot may or may not hold a capability. (Unless we say that all slots hold a capability and such a capability may by the NULL cap. The user manual seems to be inconsistent here. I think the kernel implementation (I don't know about the proof) really does have "Null caps" and I think since it does this should be documented as such. And a capability address to a NULL cap is different from a capability address that does not resolve to any slot at all.

Possibly I'm making this bigger than the specific problem.

[bennoleslie]

Since we are taking confusing things around capabilities. One things that has confused me in the past is that inside the kernel there are various variations on the theme of capPtr. This is not related to the CPtr described in the manual.

I know there is a distinction between interface and implementation, but having cptr at user level and referring to a capability address and having the not exactly the same, but pretty similar, capptr in the kernel, but pointing to an actual kernel object is certainly confusing as you jump between levels.

[bennoleslie]

And on the same line. badge is also confusing in for example seL4_CNode_Mutate. Given it is a badge or a guard, we should call it data (which is what it is in the kernel).

[lsf37]

The manual is actually wrong there (see RFC-7), you can only provide a guard in Mutate.

[bennoleslie]

The manual is actually wrong there (see RFC-7), you can only provide a guard in Mutate.

Oh, right. There is the magical "preserve" parameter to updateCapData that I didn't see. Seems like pivot is in the same boat. I couldn't understand from either RFC-7 or SELFOUR-136 the reason why Mutate/CNode has 'preserve=True'. And why there are special semantics for preserving some cap datas but not others.

[lsf37]

Finally found the commit that introduces preserve in Haskell. It's from 2007, and it look like it was actually a bug discovered during the proof: changing the badge can change the CDT parent/child relationship, and during a move operation we do not want that to happen.

During a copy operation, we're modifying that relationship anyway, because we are constructing a new cap, so that is why it
is allowed there.

[lsf37]

(The reason changing the badge changes parent/child is that a neighbour cap to the same object with a non-zero badge is treated as a child of a zero-badge cap -- all of this is because there are not enough bits on 32-bit architectures to properly represent depth in the CDT. It'd be good, but at least a medium-sized operation to find a better mechanism for this.)

[bennoleslie]

It's 14 years ago, but, was there any consideration at the time to simply not call updateData at all on Mutate/Rotate and remove the argument completely? The only cap type that ends up supporting updateData on 'Mutate'/'Rotate' is CNode.

[lsf37]

Yes, that's right, hence RFC-7. 14 years ago we were expecting to produce further cap types with potentially more cap data, so removing it then would have been premature.

But, there is actually a good point on the discussion on RFC-7: if we remove it, we cannot produce revokable CNode caps with guards any more. And that is probably a show-stopper for removing it. At least I haven't come up yet with anything that would suitably replace it. If that is the case, we should probably rename the operation, but otherwise leave it as is.