On 22 Aug 2021, at 10:34, Mark Jones <m...@pdx.edu<mailto:m...@pdx.edu>> wrote:
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. Mutate has always been a strange name for it, I agree. In fact, I think it would be best to remove the entire operation. 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. Yes, this operation never was able to change cap rights, the manual is just wrong there. I don't think there is anything inherent in the model that makes it necessary, it was a pure design decision, and in fact I used to believe that it can change rights here https://sel4.atlassian.net/browse/SELFOUR-136, but I was wrong there, too :-) (I checked, even the very first spec draft in 2006 did already not do this). 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 ...) Your test is correct. The spec also says that if the cap is moved, badges can't change, and mutate does move it. Mutate *was* able to also mint badges in the past, but that was removed around 2008, so even before the first release. This is probably where the manual has that remnant from. 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. That is currently correct. My guess is that the initial idea was to update any user-settable cap data, but it turned out that there isn't much data in caps that would make sense to be mutable, and the notion of mutable caps is somewhat strange in itself. 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. Yes. One conclusion is that the manual's description of Mutate probably needs an update. At the very least, yes. 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)? My vote would be for removing it. I'll put up an RFC for it. Cheers, Gerwin _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
