MSR_HV_SIEFP
orig = RDMSR(MSR_HV_SIEFP);
WRMSR(MSR_HV_SIEFP, val);
WRMSR(MSR_HV_SIEFP, (orig & MSR_HV_SIEFP_RSVD_MASK));