rdmsrl is really misnamed. It should have been rdmsrq to be consistent, and have rdmsrl return the low 32 bits.
So if you would prefer u64 rdtsc64(), u32 rdtsc_low(), u64 rdmsr64(int
msr), u32 rdmsr_low(int msr), I can convert everyone to that, although
it's a more invasive change...
I prefer the more explicit linux-style naming of rdmsr_low32/rdmsr64,
myself, even though this is x86-specific code. Noone has an excuse for