ipi_mbox_t
const size_t len = ncpu * sizeof(ipi_mbox_t);
put_msg(ipi_mbox_t *mbox, ipi_msg_t *msg)
ipi_mbox_t *mbox = &ipi_mboxes[cpu_index(ci)];
static ipi_mbox_t * ipi_mboxes __read_mostly;