On Sun, Oct 12, 2025 at 09:21:44AM -0700, H. Peter Anvin wrote:
MSR_TSC_AUX is a 32-bit register,
Every MSR is 64-bit. This one has bits [63:32] reserved. :-P :-P But yeah, TscAux is [31:0]...
so the two actions are *exactly identical*. This seems like a misunderstanding that has propagated through multiple texts, or perhaps someone thought it was more "future proof" this way.
I think the Intel documentation is even crazier and says "the low 32 bits of IA32_TSC_AUX"...
Well, funny you should mention that - this raises a good question: what happens in the future if we want to put the whole u64 into the destination reg of RDPID?
Should we extend the insn now, while the high u32 is reserved and is a don't care?
Because I can already see the CPUID bits and such saying: "this RDPID flavor reads the whole u64 MSR, yadda yadda..."
If we fix it now, there's no need for any of that.