On Mon, 2024-12-16 at 10:30 +0000, Indan Zupancic wrote:
Hello yf,
On 2024-12-15 21:52, Yanfeng Liu wrote:
I was wondering how to get total unused space of an untyped object? My understanding is to follow the linked list from the untyped and sum up free space of all encountered untyped nodes. is this the right approach?
That would work, but is overly complicated. The UT cap has a field capFreeIndex which says from where on the memory is free. That together with the size of the UT found in capBlockSize gives you enough information.
Thanks for this information. Here I use it to get unused space for an Untyped object as `((1 << capBlockSize) - (capFreeIndex << seL4_MinUntypedBits))` following above information. I also sum up the size of all unique Frame objects (indexed by capFrameBasePtr) as spaces used for Frames. Then I noticed at some point of `sel4test-driver` app, the sum of total free Untyped in all CSpaces plus total unique frame size is still far less than total size of all original Untypeds. I am wondering how can we explain this gap?
thanks, now I take that two adjacent nodes in mdbNext linked list should be either `parent-child` or `sibling` relationship, right?
No, because there is only one tree and the depth of the tree can be more than 3 deep. Have a look at Figure 3.1: "Example capability derivation tree" in the manual.
Thank you Indan, you have been very helpful.
You're welcome.
Indan
Regards, yf