Gerwin Klein ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3A53da0a... ) *created* an issue

RFCs ( https://sel4.atlassian.net/browse/RFC?atlOrigin=eyJpIjoiZTVmNzU0Y2NiZTc0NDkw... ) / RFC ( https://sel4.atlassian.net/browse/RFC-7?atlOrigin=eyJpIjoiZTVmNzU0Y2NiZTc0ND... ) RFC-7 ( https://sel4.atlassian.net/browse/RFC-7?atlOrigin=eyJpIjoiZTVmNzU0Y2NiZTc0ND... ) Removing CNode_Mutate ( https://sel4.atlassian.net/browse/RFC-7?atlOrigin=eyJpIjoiZTVmNzU0Y2NiZTc0ND... )

Issue Type: RFC Assignee: Gerwin Klein ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3A53da0a... ) Created: 22/Aug/21 11:31 AM Reporter: Gerwin Klein ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3A53da0a... )

Summary -------

This RFC proposes to remove the API seL4_CNode_Mutate()

Motivation ----------

CNode_Mutate does not do what the manual describes (a combination of move and and setting badge). The only action CNode_Mutate can currently take that CNode_Move cannot take is setting the guard of a CNode , which can also be done via CNode_Mint (where CNode_Mint would be copying the cap – if you wanted the same effect, you could afterwards delete the cap it was copied from).

Guide-level explanation -----------------------

seL4_CNode_Mutate() is mostly unused and has no use cases that cannot already be achieved with other API calls. The current description of seL4_CNode_Mutate() in the manual is incorrect.

Drawbacks ---------

I suspect there are no real drawbacks. It is theoretically possible that there is an application out there that makes extensive used of re-setting guards on CNodes while not copying the CNode caps, but that sounds unrealistic.

Rationale ---------

Different options would be to extend CNode_Mutate to allow changing badges, and possibly even to allow changing cap right. If we wanted to, we could even allow an in-place update. As the discussion in SELFOUR-136 indicates, mutating an existing cap is not a good fit for the cap model in general and makes reasoning about caps harder.

The minimal action would be to do nothing and only update the manual to reflect that CNode_Mutate has almost no useful purpose.

( https://sel4.atlassian.net/browse/RFC-7#add-comment?atlOrigin=eyJpIjoiZTVmNz... ) Add Comment ( https://sel4.atlassian.net/browse/RFC-7#add-comment?atlOrigin=eyJpIjoiZTVmNz... )

Get Jira notifications on your phone! Download the Jira Cloud app for Android ( https://play.google.com/store/apps/details?id=com.atlassian.android.jira.cor... ) or iOS ( https://itunes.apple.com/app/apple-store/id1006972087?pt=696495&ct=Email... ) This message was sent by Atlassian Jira (v1001.0.0-SNAPSHOT#100174- sha1:8523140 )