Hi, Mark! (Apologies if you get this twice--I tried on Sunday (UTC+1000) to send it to the list, but it disappeared.) At 2021-08-21T17:34:44-0700, Mark Jones wrote:
But a comment in the (Haskell version of the) spec says "endpoint capabilities may not have their badges changed" when they are updated by a Mutate or Rotate operation. And the kernel seems to follow this: I added a test to sel4test to confirm that you get an illegal operation error if you try to badge an endpoint using Mutate. (Assuming I wrote the test correctly ...) [...] One conclusion is that the manual's description of Mutate probably needs an update. But if nobody else has tripped over problems using it to create badged endpoints, then perhaps Mutate just isn't being used very much at all and could be removed altogether? A second thought is whether Mutate could be modified to perform an in-place update if the source and destination are the same (i.e., similar in some ways to how you specify a swap with Rotate)?
I'm glad you mentioned Rotate. Last I checked the only place it was
used in any seL4 project was in the kernel's test suite.
And it's good that it's there, since it is an exposed interface and
absolutely should be tested, but the bad news is that we have no
demonstrable use cases for it. When I asked around about it, there were
some recollections that it was thought necessary, either for logical
completeness or to avoid a wasteful context switch (much as seL4 has
many more than just the "fundamental" three system calls[1], but also
fused calls like ReplyRecv to cut down on round trips through the
kernel). But I was unable to pin down anything authoritative enough to
put in writing from the authorities available to me.
Can you supply such a use case? I think that while we're cleaning up
the system call picture as Gerwin suggested, we could do with having
model uses for the calls that remain. (I was reviewing the Austin
Group's latest draft of Issue 8 lately, and was surprised at how obvious
some of their examples for library functions like rename() are. But
then I remembered, that if you don't show people the most obvious and
intended way to use an interface, some will manage to come up with
amazingly obfuscated ones.)
Regards,
Branden
[1] https://sel4.systems/Info/Docs/seL4-manual-latest.pdf
On Sun, Aug 22, 2021 at 10:38 AM Mark Jones
This isn't a big issue, but I'm curious about how seL4_CNode_Mutate is intended to be used, and have found that the description in the seL4 reference manual doesn't seem to match the implementation.
Is it for changing rights? The manual (Section 3.1.2) says: "seL4_CNode_Mutate() can move a capability similarly to seL4_CNode_Move() and also reduce its rights..." Section 3.1.4 also refers to the possibility to specify a new set of rights with an invocation of seL4_CNode_Mutate(). However, the summary of seL4_CNode_Mutate in Section 10.3.1.6 does not include a parameter that specifies any rights information, so it appears that it cannot actually be used in this way.
Is it for changing badges? In Section 4.2.1, the manual says that "An endpoint capability with a zero badge ... can be badged with the seL4_CNode_Mutate() or seL4_CNode_Mint() invocations" There is a similar statement for Notifications in Section 5.1. But a comment in the (Haskell version of the) spec says "endpoint capabilities may not have their badges changed" when they are updated by a Mutate or Rotate operation. And the kernel seems to follow this: I added a test to sel4test to confirm that you get an illegal operation error if you try to badge an endpoint using Mutate. (Assuming I wrote the test correctly ...)
Unless there are other arch-specific use cases, it looks like the only thing you can do with Mutate is to change the guard of a CNode capability. Even then, that is only possible if you are moving the capability at the same time. Of course, you could combine a mutate with a regular move to simulate an in-place update ... but you could also use an in-place mutate and a separate move to simulate the current behavior, without having to find an empty slot if you just wanted the in-place operation.
One conclusion is that the manual's description of Mutate probably needs an update. But if nobody else has tripped over problems using it to create badged endpoints, then perhaps Mutate just isn't being used very much at all and could be removed altogether? A second thought is whether Mutate could be modified to perform an in-place update if the source and destination are the same (i.e., similar in some ways to how you specify a swap with Rotate)?
Best wishes, Mark
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems