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