In helper_rdmsr(), access to TSC_AUX is enabled only if TARGET_X86_64. I guess it should not be so. In helper_wrmsr(), it is OK.