Why does seL4_TCB_CopyRegisters exist?

seL4 kernel
1

The seL4_TCB_CopyRegisters provides an atomic copy of registers between two TCBs (and has a somewhat dated interface). It’s not clear in what circumstances this is necessary. This might help in situations where you want fork-like semantics without the address space copy, but there doesn’t seem to be any real justification.

The existence of this invocation does seem to have induced a bit of unnecessary complexity into the kernel.

2

In circumstances where you would want to read or write registers, there are few where this happens between two existing TCBs rather than into and out of memory (such as checkpointing).