[seL4] Re: CDT traveling

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