Hi,

I have a design question regarding how to recycle capabilities/memory frames that were used by a thread once it terminates.

Let's assume that there is a MemoryManager server responsible to serve virtual memory to user processes (e.g similar to implementing VirtualAlloc).

The MemoryManager has to maintain the list of untyped object, retype them, maintain likely a list of resources allocated for a user thread, likely copy/mint the page frames to forward them to the user process...etc.

But when a thread terminates, as I can't see any related events in seL4, I would assume that the user process would have to explicitly notify the MemoryManager on exit.

Then the MemoryManager would know which user thread has exited and would update/recover the used capabilities and destroy them, in order to recover untyped objects.

Would it be a proper design that plays well with seL4? Do you think that it could be done more efficiently with seL4?

Thank you!