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

Hi Yadong,

On 12 Dec 2021, at 03:09, yadong.li wrote:

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 ?

The Zombie cap is only created for CNode B if the cap to B in CNode A was the last (final) cap to CNode B in the system. Otherwise, the cap is just deleted, removed from the CDT (capability derivation tree) and replaced with a NullCap. In the scenario above, this means component B does not have a cap any more to CNode B and therefore can't operate on it. One of the invariants we proved about the kernel is that all Zombie caps are final: https://github.com/seL4/l4v/blob/ce67a725f7fca0ea40803d58ff5706ce30b005ad/pr...

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 ?

The special status of slot 0 is just a user-level convention, the kernel assigns no special status to slot 0. It uses slot 0 only when user-level cannot access it any more. If I remember correctly, the convention of the current user-level libraries is that if a thread has a cap to its own CSpace it would usually be stored in slot 0. But it is only a convention. Cheers, Gerwin