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
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
gives also some useful details.