Hi Yadong, > On 12 Dec 2021, at 03:09, yadong.li <[email protected]> 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/proof/invariant-abstract/Invariants_AI.thy#L781-L786 > 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 _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
