/* Executes a WBINVD instruction. This function is only available on IA-32 and X64.  */
VOID EFIAPI AsmWbinvd(VOID)
/* Executes a WBINVD instruction. This function is only available on IA-32 and X64.  */
VOID EFIAPI AsmWbinvd(VOID)
{
  __asm__ __volatile__ ("wbinvd":::"memory");
}