HP_NAME_MDS_LEAVE
HOTPATCH(HP_NAME_MDS_LEAVE, MDS_LEAVE_BYTES) ; \
.name = HP_NAME_MDS_LEAVE,
x86_hotpatch(HP_NAME_MDS_LEAVE, /* nomds */ 0);
x86_hotpatch(HP_NAME_MDS_LEAVE, /* mds */ 1);