EX_SIZE
u64 exgen[EX_SIZE] __attribute__((aligned(0x80)));
u64 exnmi[EX_SIZE]; /* used for system reset (nmi) */
u64 exmc[EX_SIZE]; /* used for machine checks */
u64 exrfi[EX_SIZE] __aligned(0x80);