VMCS_EOI_EXIT1
vmcs_write(VMCS_EOI_EXIT1, ((uint64_t)tmrs[3] << 32) | tmrs[2]);
vmcs_write(VMCS_EOI_EXIT1, 0);