[seL4] Re: seL4 kernel memory footprint

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.

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