These registers are part of the 'regular' TCB state and are saved and restored as part
of normal thread switching. As such it is conflicting to have a duplicate idea of the value
of these registers, especially as it is not kept in sync with the version in the TCB,
which is what is actually being loaded into the hardware.