Hello yf,
On 2024-12-13 05:51, Yanfeng Liu via Devel wrote:
can we take that:
- non-zero `mdbNext` must pointer to entries in CNodes or TCB blocks?
If you mean that the derivation tree is build with caps, and those
reside in either CNodes slots or in special slots in the TCB, then yes.
- sum of free spaces of untypeds in a list depicts free space for the
list?
Not sure what you mean. There is only one list, and it is a linked list.
You allocate memory for list nodes when you allocate CNode or TCB
objects
from untypeds.
`isMDBParentOf` can judge parent/child relationship. what other
non-parent/child
relationships are there in this `mdbNext` link?
That one should cover all cases.
Where can we find more information about the flattening?
Talking to people and reading the kernel source code.
As far as I know there is no detailed design paper.
Over time little details in the manual will make more
sense when you reread it, because you get a better
understanding how everything fits together. Same for
the code.
Greetings,
Indan
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
