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
On 22 Aug 2021, at 10:34, Mark Jones <mpj@pdx.edumailto:mpj@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
See now https://sel4.atlassian.net/browse/RFC-7
If there are arguments why we should keep CNode_Mutate, please comment there.
Cheers, Gerwin
On 22 Aug 2021, at 11:15, Gerwin Klein <kleing@unsw.edu.aumailto:kleing@unsw.edu.au> wrote:
On 22 Aug 2021, at 10:34, Mark Jones <mpj@pdx.edumailto:mpj@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
"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."
Not really strange... IMHO there can be very specific scenarios (in a MCS?) where having such flexibility could be useful. I know it is dangerous, but it may be useful. Before killing that feature (currently not implemented) I would research potential applications.
El dom, 22 ago 2021 a las 3:35, Gerwin Klein (kleing@unsw.edu.au) escribió:
See now https://sel4.atlassian.net/browse/RFC-7
If there are arguments why we should keep CNode_Mutate, please comment there.
Cheers, Gerwin
On 22 Aug 2021, at 11:15, Gerwin Klein <kleing@unsw.edu.aumailto: kleing@unsw.edu.au> wrote:
On 22 Aug 2021, at 10:34, Mark Jones <mpj@pdx.edumailto:mpj@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
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 mpj@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.
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
On 23 Aug 2021, at 18:16, Branden Robinson g.branden.robinson@gmail.com wrote:
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.
Similar to Mutate ;-)
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.
As far as I remember, the use case was (in a dynamic system) a CSpace manager for another thread T wanting to change a sub-space of T's CSpace. That is, replacing an existing CNode cap in T's space with another CNode cap, to a different (previously prepared) CNode.
With Rotate you can do that while T is running, because the replacement is atomic within one syscall. Without Rotate, you need at least to Move operations, and in between those two operations, T might be looking up caps and fail because of it.
We haven't built any larger such systems, so Rotate is definitely currently underused.
The (remaining) use case for Mutate is to change the guard of an existing cap.
My argument was that you can do this with Mint + Move, and this time there does not seem to be a scenario for atomicity.
It has been pointed out on the RFC in the meantime that there is one thing that removal of Mutate would take away: after Mutate you can still revocably copy, after Mint + Move you cannot.
Cheers, Gerwin
-
Branden Robinson -
Gerwin Klein -
Hugo V.C. -
Mark Jones