Hi Gerwin： First of all, thank you for your help About the check "preemptionPoint", thank you for your answer, I think I did not recognize the change of ThreadState correctly from the beginning. About the cteDelete question, from your answer, I think I get the core concept of the deletion and finalisation, when cnode object become cyclic zombie, it will actual delete when the untyed memory(the last ref) of the cnode object was revoked. But I still not sure about some of the behavior, Imaging the following scenairo: The cspace of compont A has a slot that store cnode object of component B(May be A is parent of B, or A is of B who get cnode of B by transfer cap), the untyped memory of cnode A is different with untyped memory of cnode B， Now if we revoke untyped memory of cnode A and we do not revoke untyped memory of cnode B .， I think the slot 0 of cnode B will store Cyclic zombie capability as our discussion， 1. At this time，I think compont B can work normally even though the cnode B become Cyclic zombie, am I right ? 2. if componet B still work, but the cap of slot 0 is changed, Does this require the user not to use slot 0 ? I found create_cspace in process.c below: static int create_cspace(vka_t *vka, int size_bits, sel4utils_process_t *process, seL4_Word cspace_root_data, seL4_CPtr asid_pool) { ....... /* first slot is always 1, never allocate 0 as a cslot */ process->cspace_next_free = 1; } Is the comments for this purpose ? Cheers, Yadong -----邮件原件----- 发件人: Gerwin Klein [mailto:kleing@unsw.edu.au] 发送时间: 2021年12月11日 7:54 收件人: yadong.li 抄送: devel@sel4.systems 主题: Re: [seL4] 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