On 20/05/19 21:01, Sean Christopherson wrote: > Would it make sense to inject a #GP if the guest attempts to set bits that > are reserved to be zero, e.g. based on guest CPUID? Yes, though it was not clear from the SDM quote that hardware enforces that (I guess the hint is that they "must" be written as zero rather than "should"). I'll include this patch in my next pull request with fixed commit message, and do the #GP change separately. Paolo