On 1 Feb 2020, at 06:47, Alexandre Mutel mailto:alexandre_mutel@live.com> wrote: 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. A thread cannot just “terminate”, it can only cease to exist if it’s TCB is removed by whoever manages it (i.e. has the right caps to the TCB). Whoever does that would have to clean up any other resources belonging to the thread. Note that this is not so different from, say, Linux. There a process can’t just vanish either, it can terminate as a result of: - an exit() syscall, telling the OS it wants to die - someone sending it a kill signal - the process throws an exception and gets killed as a result. In any case, this requires an OS invocation, either by a syscall or an exception (which can be seen as an implicit syscall). Your seL4-based OS will have to do similar things. Unlike Linux, your OS may consist of several servers responsible for different resources, which mean they will have to coordinate. Gernot