On Thu, 2024-12-12 at 13:29 +0000, Indan Zupancic wrote: > Hello, > > On 2024-12-12 12:42, Yanfeng Liu via Devel wrote: > > I noticed that `mdb_node_t` has `mdbPrev` and `mdbNext` pointer fields > > but > > not sure how can they be used to travel the capability derivation tree? > > The capability derivation tree is flattened into a list. > Thank you Indan!
can we take that: - non-zero `mdbNext` must pointer to entries in CNodes or TCB blocks? - sum of free spaces of untypeds in a list depicts free space for the list? > The kernel knows whether a node is a child node or not > depending on the type and data of the cap and object. > > Greetings, > > Indan Regards, yf _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
