At 2019-04-17T12:21:41+0000, Leonid Meyerovich wrote:
Is there any way in seL4 (library function?) to check free heap memory?
My understanding is that there is not, because the seL4 microkernel does not implement a memory manager. A malloc()-style memory manager is not considered an essential service for a microkernel, so seL4 leaves the provision of such a service up to the implementation.
The seL4 FAQ says the following:
"How can usermode manage kernel memory safely?
The kernel puts userland in control of system resources by handing all free memory (called ‘‘Untyped’’) after booting to the first user process (called the ‘‘root task’’) by depositing the respective caps in the root tasks’s Cspace. The root task can then implement its resource management policies, e.g. by partitioning the system into security domains and handing each domain a disjoint subset of Untyped memory.
If a system call requires memory for the kernel’s metadata, such as the thread control block when creating a thread, userland must provide this memory explicitly to the kernel. This is done by ‘‘retyping’’ some Untyped memory into the corresponding kernel object type. Eg. for thread creation, userland must retype some Untyped into ‘‘TCB Objects’’. This memory then becomes kernel memory, in the sense that only the kernel can read or write it. Userland can still revoke it, which implicitly destroys the objects (eg threads) represented by the object.
The only objects directly accessible by userland are ‘‘Frame Objects’’: These can be mapped into an ‘‘Address Space Object’’ (essentially a page table), after which userland can write to the physical memory represented by the Frame Objects."
https://docs.sel4.systems/FrequentlyAskedQuestions.html
A "memory server" that hands out chunks of "heap memory" to threads requesting it would likely be a part of any even vaguely Unix-like kernel running on top of seL4. Even better, the memory server you implement (or otherwise obtain) can implement a policy that avoids over-commitment of memory, which is a notorious source of reliability problems on Linux and other Unix kernels. If you search LWN.net for the term "OOM killer" [out-of-memory process killer], you will find articles documenting Linux's struggle with the consequences of memory over-commitment going back at least 15 years. It is an active struggle today; see, for example, https://lwn.net/Articles/761118/ .
A quick glance suggests to me that there isn't a ready-made heap-like memory server available as a CAmkES component[1], but if I'm mistaken I urge someone to speak up and correct me.
Regards, Branden