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 <[email protected]> > 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 > >
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
