[seL4] Re: seL4 kernel memory footprint

On Sun, Jul 10, 2022 at 3:04 PM Sam Leffler wrote:

On Fri, Jul 8, 2022 at 6:38 PM Gernot Heiser wrote:

...

On 9 Jul 2022, at 05:15, Sam Leffler via Devel wrote:

...

I'm trying to figure out the physical memory used by the kernel. This is for riscv if it matters.

Hi Sam,

The RAM usage of the kernel is dominated by application specifics.

I don't think so, but perhaps I misunderstand what "application specifics" means. The memory footprint of the _kernel_ (not anything running in use space) appears to be fixed at the point where it launches the rootserver (+idle thread). Or does the kernel dynamically allocate memory _after_ starting the rootserver?

...

The kernel, at boot time, allocates enough RAM to boot up and start the init task. That’s it’s own text segment, its own page tables, a small amount of global data, and a kernel stack per core, plus whatever’s needed for init. (No heap!) It’s a while we’ve done an audit, but should fit into 64KiB.

Is 64KB what you expect for a release build up to the point where the rootserver setup happens? What target cpu + config? Does this include the idle thread? This is substantially less than my release build for riscv w/ MCS but I enable CONFIG_PRINITING and we have a few drivers (timer, uart) though they should be small. IIRC the ELF headers for our release kernel.elf have a load segment ~110KB.

The ELF load segment # is misleading 'cuz it includes the rootserver image which in turn includes the CAmkES compoents. So 110KB might make sense relative to 64KB for the kernel proper. Will check.

...

This is normally dominated by what you need to run an actual system: for each user process you’ll need - page tables - TCB(s) - Cspace - other objects, such as endpoints, Notifications

These are provided to the kernel by re-typing Untypeds, and as such the responsibility of usermode.

Sure. I believe I'm reclaiming all rootserver resources so once it terminates I expect to see all of physical memory accounted for by the kernel, idle thread, rootserver-allocated resources (to construct CAmkES components), and unallocated memory held by untyped objects. But I don't know for sure what the kernel portion is and the total "reserved" memory seems high. Hence my ask.

I don't suppose there's some kernel variable I can print that will help answer my q?

...

Gernot _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems