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


Indeed, never thought in the details about how an OS was handling this, but I can see the same behavior in Linux and it makes complete sense. I had also a look at the design document https://github.com/rticommunity/libsel4osapi/blob/master/docs/design.md  and it gives also some useful details.
Thank you!