Hello yf, On 2024-12-17 06:26, Yanfeng Liu wrote:
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?
sel4test creates a lot of threads and objects, it doesn't create that much frames in general, except for the frame tests, so I would say that what you see is to be expected for sel4test. It's not like a typical program which would mostly use heap memory. Greetings, Indan