On Wed, Jan 23, 2019 at 6:06 AM Yang Weijiang <weijiang.yang@xxxxxxxxx> wrote: > Note: Although these VMCS fields are 64-bit, they don't have high fields. This statement directly contradicts the SDM, volume 3, appendix B.2: "A value of 1 in bits 14:13 of an encoding indicates a 64-bit field. There are 64-bit fields only for controls and for guest state. As noted in Section 24.11.2, every 64-bit field has two encodings, which differ on bit 0, the access type. Thus, each such field has an even encoding for full access and an odd encoding for high access."