Yes, I, probably, was not specific enough. My question was not about kernel memory. I'd like to have something to support memory leak investigation, for the memory which is allocated by malloc (libmuslc library). BTW, how libmuslc get memory for memory management? Thank you, Leonid -----Original Message----- From: Devel On Behalf Of Heiser, Gernot (Data61, Kensington NSW) Sent: Wednesday, April 24, 2019 2:18 AM To: devel@sel4.systems Subject: Re: [seL4] seL4 process memory utilization Banden’s answer is correct, tl;dr you cannot check the available space in the kernel heap as there is no kernel heap. However, Leonid's initial question was somewhat ambiguous. The various seL4 userland frameworks inevitably provide their own (usually pretty unsophisticated) memory managers, which maybe global (in which case you lose most of the kernel-enforced isolation) or per-process. If you’re using one of those then they may or may not provide a method for checking the amount of remaining free memory (and if they don’t it would probably be pretty easy to add). Leonid, you may want to clarify what you meant. Gernot

On 24 Apr 2019, at 04:33, G. Branden Robinson wrote:

Signed PGP part 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

[1] https://github.com/seL4/camkes/tree/master/apps

________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

Thank you, I’ll look into it. From: Matthew Fernandez Sent: Thursday, April 25, 2019 11:15 AM To: Leonid Meyerovich Cc: Heiser, Gernot (Data61, Kensington NSW) ; devel@sel4.systems Subject: Re: [seL4] seL4 process memory utilization On 24 Apr 2019, at 07:20, Leonid Meyerovich mailto:lmeyerovich@i-a-i.com> wrote: Yes, I, probably, was not specific enough. My question was not about kernel memory. I'd like to have something to support memory leak investigation, for the memory which is allocated by malloc (libmuslc library). BTW, how libmuslc get memory for memory management? Thank you, Leonid This isn’t quite what you want, but if it’s still functional there’s a rudimentary heap debugger I wrote a while back. You might be able to bend it to your purpose. https://github.com/seL4/seL4_libs/blob/master/libsel4debug/src/alloc.c ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.