On 2024-12-17 12:59, Yanfeng Liu wrote:
I further checked the types of `mdbNext` and `mdbPrev` node of Untyped objects in the lists and noticed that most of them are of `Untyped` and `Frame` types! This is ture for several seL4 demos including sel4test.
As per manual, Untyped can be split as smaller Untypeds and retyped to other objects.
If you look at the start of the list, you're probably looking at device memory regions. To allocate a specific physical address, all memory from the start of the beginning of an UT up to the target address needs to be allocated in power of 2 UT chunks. Only then an allocation of a frame will match the target physical address. That is probably why you see so many UTs in between Frame objects. This awkwardness is caused by untyped requiring power of 2 size and alignment. (I have a fix for that in PR #1363, but that will need a lot of time and funding for the verification changed.)
I can't understand why many `Frame` objects are before Untyped objects? maybe those Frame objects before Untyped objects aren't related to the latter, they are there due to the flattening effect only?
All objects are between UTs, so I'm not sure what you mean. If a Frame comes before an UT, it just means it is the last allocation in a previous UT. I recommend skipping all device memory UTs when looking at the list. Greetings, Indan