[seL4] Re: two questions about cteDelete of sel4 kernel 12.0.0 ?

On 11 Dec 2021, at 04:02, yadong.li wrote:

Very good questions, deletion and finalisation are one of the most intricate algorithms in seL4.

1. I think when call capSwapForDelete in reduceZombie, the level 2 cnode become Cyclic zombie, but when return finaliseSlot, I do not think it will deal with below branch: if (!immediate && capCyclicZombie(fc_ret.remainder, slot)) { } because this time ,slot ->cap is not cnode or tcb, it will not create zombie cap. Who will delete level 2 cnode ? Is it lost as "Cyclic zombie", memory leak?

Deleting a final CNode cap is only guaranteed to fully finalise that one CNode, not recursively all CNodes that are mentioned in it. This is by design, because CNodes are a potentially cyclic graph, not necessarily a tree, and fully traversing them is not necessary for cap deletion (see below). It is correct that the cteDelete/finalise functions will create cyclic Zombie caps for level 2 CNodes (in the terminology above). This is safe and does not lead to a memory leak, because the finalise functions don't delete objects, they only delete capabilities and reset objects to a final state. The condition that cteDelete and finalise need to establish is that when the last capability to an object is removed, the object becomes truly inaccessible and inactive. The main condition for this is that no other object or global state in the kernel points to that object any more. This is why finalise calls all kinds of "unbind" and "reset" operations on objects. The actual deletion of objects and reclaiming of memory only happens later at "retype" when memory is cleared. The retype operation is an invocation of the Untyped cap to that area of memory. Untyped capabilities track all other capabilities that point to objects in the area the Untyped cap is responsible for, so the way to reclaim and reuse memory is to call "revoke" on that Untyped cap, which will call capDelete on all descendant caps, and leave the entire memory area of that Untyped ready for retyping. In summary: - Deleting a single cap is not intended to be an operation that helps much with reclaiming memory. It is an operation to remove authority. Finalisation is a necessary potential side effect of deleting a cap, because removing the last cap to an object is the last chance the kernel has to properly clean up state for that object. - The operation that is intended for reclaiming memory is the combination of Untyped revoke + retype.

2. when delete cnode, it will check "preemptionPoint", if our delete is beak, even though fs_ret.success is false, but this false is not deliver to caller, who will delete cnode object again?

I'm not entirely sure which scenario you mean, but there are two main ones, I think: 1) if you mean the level 1 CNode that is being finalised, then a preemption will leave the syscall in a state where the caller now holds a Zombie cap to the level 1 CNode, and that Zombie cap tracks how much progress has been made. If the caller gets to run again, it gets restarted at the same program counter as before, which means the syscall is restarted with the Zombie cap, and deletion progresses. 2) if you mean the level 2 CNode, and there were no other capabilities to it in the system, which means there is only the cyclic Zombie cap to it left, then a "revoke" call on the Untyped cap guarding that memory will finalise that Zombie cap and continue finalisation of the level 2 CNode at that point. Cheers, Gerwin