Dear experts, I am trying to understand the memory usage of a running seL4 demo with help of GDB. I am wondering how I can travel the Capability derivation tree starting from original untyped objects and see how memory are used. I noticed that `mdb_node_t` has `mdbPrev` and `mdbNext` pointer fields but not sure how can they be used to travel the capability derivation tree? Regards, yf
Hello, On 2024-12-12 12:42, Yanfeng Liu via Devel wrote:
I noticed that `mdb_node_t` has `mdbPrev` and `mdbNext` pointer fields but not sure how can they be used to travel the capability derivation tree?
The capability derivation tree is flattened into a list. The kernel knows whether a node is a child node or not depending on the type and data of the cap and object. Greetings, Indan
On Thu, 2024-12-12 at 13:29 +0000, Indan Zupancic wrote:
Hello,
On 2024-12-12 12:42, Yanfeng Liu via Devel wrote:
I noticed that `mdb_node_t` has `mdbPrev` and `mdbNext` pointer fields but not sure how can they be used to travel the capability derivation tree?
The capability derivation tree is flattened into a list.
The kernel knows whether a node is a child node or not depending on the type and data of the cap and object.
Thank you, I think you are talking about `mdbNext` lists. I noticed `isMDBParentOf` can judge parent/child relationship. what other non-parent/child relationships are there in this `mdbNext` link? Where can we find more information about the flattening?
Greetings,
Indan
Regards, yf
On Thu, 2024-12-12 at 13:29 +0000, Indan Zupancic wrote:
Hello,
On 2024-12-12 12:42, Yanfeng Liu via Devel wrote:
I noticed that `mdb_node_t` has `mdbPrev` and `mdbNext` pointer fields but not sure how can they be used to travel the capability derivation tree?
The capability derivation tree is flattened into a list.
Thank you Indan! can we take that: - non-zero `mdbNext` must pointer to entries in CNodes or TCB blocks? - sum of free spaces of untypeds in a list depicts free space for the list?
The kernel knows whether a node is a child node or not depending on the type and data of the cap and object.
Greetings,
Indan
Regards, yf
Hello yf, On 2024-12-13 05:51, Yanfeng Liu via Devel wrote:
can we take that: - non-zero `mdbNext` must pointer to entries in CNodes or TCB blocks?
If you mean that the derivation tree is build with caps, and those reside in either CNodes slots or in special slots in the TCB, then yes.
- sum of free spaces of untypeds in a list depicts free space for the list?
Not sure what you mean. There is only one list, and it is a linked list. You allocate memory for list nodes when you allocate CNode or TCB objects from untypeds.
`isMDBParentOf` can judge parent/child relationship. what other non-parent/child relationships are there in this `mdbNext` link?
That one should cover all cases.
Where can we find more information about the flattening?
Talking to people and reading the kernel source code. As far as I know there is no detailed design paper. Over time little details in the manual will make more sense when you reread it, because you get a better understanding how everything fits together. Same for the code. Greetings, Indan
On Sat, 2024-12-14 at 22:56 +0000, Indan Zupancic wrote:
Hello yf,
On 2024-12-13 05:51, Yanfeng Liu via Devel wrote:
can we take that: - non-zero `mdbNext` must pointer to entries in CNodes or TCB blocks?
If you mean that the derivation tree is build with caps, and those reside in either CNodes slots or in special slots in the TCB, then yes.
- sum of free spaces of untypeds in a list depicts free space for the list?
Not sure what you mean. There is only one list, and it is a linked list. You allocate memory for list nodes when you allocate CNode or TCB objects from untypeds.
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?
`isMDBParentOf` can judge parent/child relationship. what other non-parent/child relationships are there in this `mdbNext` link?
That one should cover all cases.
thanks, now I take that two adjacent nodes in mdbNext linked list should be either `parent-child` or `sibling` relationship, right?
Where can we find more information about the flattening?
Talking to people and reading the kernel source code. As far as I know there is no detailed design paper. Over time little details in the manual will make more sense when you reread it, because you get a better understanding how everything fits together. Same for the code.
Greetings,
Indan Thank you Indan, you have been very helpful.
Regards, yf
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, 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
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
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
On Tue, 2024-12-17 at 11:44 +0000, Indan Zupancic wrote:
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.
Thank you. 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. 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?
Greetings,
Indan
Regards, yf
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
participants (2)
-
Indan Zupancic -
Yanfeng Liu