See commit 766b21e8fd83b5c4fcebfda809d1862dcfab54cc
It appears that we have to call Revoke on the untyped cap, regardless of whether the children of the untyped have been deleted. We always delete the children before releasing the untyped, but it seems that just deleting the children is insufficient for releasing the untyped. seL4 actually seems to require you to call Revoke on the untyped itself.
I'm not totally sure if this is correct, but this does seem to fix a bug where deleting a page wouldn't actually release the untyped from which the page is derived, so later when this "free" untyped is being retyped we have an error. The scenario is as follows: suppose we retype an untyped cap into page cap cap0, copy cap0 into cap1 and then delete cap0. It seems that simply deleting cap1 now is insufficient to release the untyped cap --- you actually have to call Revoke on the untyped itself to release it. My understanding of seL4 is very superficial so it could be that there is a subtle bug in our code base and somehow the cap tree accounting is botched. If any one is familiar with seL4, please let me know if this is correct.
cl91
commented
6 months ago
See commit 766b21e8fd83b5c4fcebfda809d1862dcfab54cc
It appears that we have to call
Revokeon the untyped cap, regardless of whether the children of the untyped have been deleted. We always delete the children before releasing the untyped, but it seems that just deleting the children is insufficient for releasing the untyped. seL4 actually seems to require you to callRevokeon the untyped itself.I'm not totally sure if this is correct, but this does seem to fix a bug where deleting a page wouldn't actually release the untyped from which the page is derived, so later when this "free" untyped is being retyped we have an error. The scenario is as follows: suppose we retype an untyped cap into page cap
cap0, copycap0intocap1and then deletecap0. It seems that simply deletingcap1now is insufficient to release the untyped cap --- you actually have to callRevokeon the untyped itself to release it. My understanding of seL4 is very superficial so it could be that there is a subtle bug in our code base and somehow the cap tree accounting is botched. If any one is familiar with seL4, please let me know if this is correct.