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 _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
