Why does seL4_TCB_CopyRegisters exist?

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.

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).