Hi Kofi, Thanks for your reply. I have modified the vspace.c to get the area for the cached sel4utils_res_t object in a configurable way. This seems to be solve my problem, but would you mind taking a look and see if I have missed something or if I'm doing something wrong? I still don't have a full understanding of the vspace/vka and memory management, so I need a second pair of eyes here. See attached diff. In short, there are 3 ways to dynamically allocate memory for the cached objects, controlled by a macro defined at the beginning of the file: - If you define MEMPOOL_USE_MALLOC will do exactly as now, it will call malloc/free to allocate the dynamic sel4utils_res_t - If you define MEMPOOL_USE_STATIC (to a numeric value), it will simply use a static pool of sel4utils_res_t objects, falling to use malloc() if this limit is reached. This was an experimental/intermediate version before I implemented the next version. - If you define MEMPOOL_USE_VSPACE will dynamically allocate pools of sel4utils_res_t objects as needed from vspace. Mapped pages are never freed, but only returned to the pool to be used later. The value of MEMPOOL_SLOT_PER_PAGE is calculated to have a whole record fit a 4k page. If the version for MEMPOOL_USE_VSPACE is correct we should probably consider integrating it. Let me know what you think. Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA On Wed, Jul 26, 2017 at 12:12 AM, wrote:

Hi Fabrizio,

I see you're getting some issues with the fact that mmap calls malloc() for its underlying reservation allocation. You're correct: it should not be doing this, and ideally there should be an object cache involved in here to handle allocation of metadata objects needed by the virtual memory management implementation.

Please wait a while and there should be a patch out soon to hopefully resolve this.

-- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

------------------------------ *From:* Devel on behalf of Fabrizio Bertocci *Sent:* 26 July 2017 07:34 *To:* devel@sel4.systems *Subject:* [seL4] Recursive call to malloc crash system

Hi all, I have a system configured to use dynamic heap through the vspace. I'm working with 5.2.0 and using pc99 simulator through qemu.

Everything is occurring in the root task, as I haven't even completed my bootstrapping code.

In this configuration, whenever my code calls malloc() and there is a low memory condition (where there is not enough space on the heap to fulfill my request), malloc() end up calling __expand_heap().

Here it first attempts to expand the heap through brk syscall, then if fails uses mmap() to attempt to get more pages from the virtual memory.

In both cases (brk and mmap) end up calling a function in the vspace that attempts to make available new pages. Unfortunately the code in the libself4utils/src/vspace/vspace.c, end up calling malloc() for the sel4utils_res structure.

As you expect, we are already in a no-memory condition, so a subsequent call to malloc() might end up calling __expand_heap() and so on... (depending on the bytes left on the heap, this nested malloc might succeed if the initial block was larger than the size of sel4utils_res structure).

So, everything loops until the whole system crash because of stack overflow.

Why vspace uses malloc() to dynamically allocate those structures, causing the whole system to fail?

To test, I have changed the implementation in vspace.c to use a static buffer pool, and it seems it solve my issue, but am I doing something wrong in the bootstrap code ?

Any help is appreciated, Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Stepping back slightly I am going to argue that fundamentally the issue here is that the heap is being used in a place where the stack should be. In this case due to vspace_new_pages having to allocate a reservation to do the mapping, only to immediately free the reservation in the same function. Having to allocate a reservation with malloc is in some ways an 'accident' of how the interfaces work, and not something that we actually want or need to happen in this case. This is something that might need to be discussed internally, as it has wider reaching impacts and breakages, but I would lean towards changing the vspace API to either * Make it possible to create reservations without involving malloc (by being able to pass a prior allocation to the reserve functions or otherwise) * Allow for passing in 'NULL' reservations to create/map pages Otherwise without changing the API doing 'self' allocation, i.e. your MEMPOOL_USE_VSPACE, instead of malloc seems reasonable, I just think it's not as 'clean' as removing the need for allocation altogether, and so think we should explore that avenue first. Adrian On Thu 27-Jul-2017 12:34 PM, Fabrizio Bertocci wrote: Hi Kofi, Thanks for your reply. I have modified the vspace.c to get the area for the cached sel4utils_res_t object in a configurable way. This seems to be solve my problem, but would you mind taking a look and see if I have missed something or if I'm doing something wrong? I still don't have a full understanding of the vspace/vka and memory management, so I need a second pair of eyes here. See attached diff. In short, there are 3 ways to dynamically allocate memory for the cached objects, controlled by a macro defined at the beginning of the file: - If you define MEMPOOL_USE_MALLOC will do exactly as now, it will call malloc/free to allocate the dynamic sel4utils_res_t - If you define MEMPOOL_USE_STATIC (to a numeric value), it will simply use a static pool of sel4utils_res_t objects, falling to use malloc() if this limit is reached. This was an experimental/intermediate version before I implemented the next version. - If you define MEMPOOL_USE_VSPACE will dynamically allocate pools of sel4utils_res_t objects as needed from vspace. Mapped pages are never freed, but only returned to the pool to be used later. The value of MEMPOOL_SLOT_PER_PAGE is calculated to have a whole record fit a 4k page. If the version for MEMPOOL_USE_VSPACE is correct we should probably consider integrating it. Let me know what you think. Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA On Wed, Jul 26, 2017 at 12:12 AM, mailto:Kofidoku.Atuah@data61.csiro.au> wrote: Hi Fabrizio, I see you're getting some issues with the fact that mmap calls malloc() for its underlying reservation allocation. You're correct: it should not be doing this, and ideally there should be an object cache involved in here to handle allocation of metadata objects needed by the virtual memory management implementation. Please wait a while and there should be a patch out soon to hopefully resolve this. -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO ________________________________ From: Devel mailto:devel-bounces@sel4.systems on behalf of Fabrizio Bertocci mailto:fabriziobertocci@gmail.com> Sent: 26 July 2017 07:34 To: devel@sel4.systemsmailto:devel@sel4.systems Subject: [seL4] Recursive call to malloc crash system Hi all, I have a system configured to use dynamic heap through the vspace. I'm working with 5.2.0 and using pc99 simulator through qemu. Everything is occurring in the root task, as I haven't even completed my bootstrapping code. In this configuration, whenever my code calls malloc() and there is a low memory condition (where there is not enough space on the heap to fulfill my request), malloc() end up calling __expand_heap(). Here it first attempts to expand the heap through brk syscall, then if fails uses mmap() to attempt to get more pages from the virtual memory. In both cases (brk and mmap) end up calling a function in the vspace that attempts to make available new pages. Unfortunately the code in the libself4utils/src/vspace/vspace.c, end up calling malloc() for the sel4utils_res structure. As you expect, we are already in a no-memory condition, so a subsequent call to malloc() might end up calling __expand_heap() and so on... (depending on the bytes left on the heap, this nested malloc might succeed if the initial block was larger than the size of sel4utils_res structure). So, everything loops until the whole system crash because of stack overflow. Why vspace uses malloc() to dynamically allocate those structures, causing the whole system to fail? To test, I have changed the implementation in vspace.c to use a static buffer pool, and it seems it solve my issue, but am I doing something wrong in the bootstrap code ? Any help is appreciated, Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel