IPI_DDB
intr_ipi_send(NULL, IPI_DDB);
case IPI_DDB:
intr_ipi_send(NULL, IPI_DDB);
case IPI_DDB:
intr_establish_xname(ARMGIC_SGI_IPIBASE + IPI_DDB, IPL_HIGH,
intr_establish_xname(IPI_DDB, IPL_HIGH, IST_MPSAFE | IST_EDGE, pic_ipi_ddb, NULL, "IPI ddb");
#define VAX_LOCK_CHECKS ((1 << IPI_SEND_CNCHAR) | (1 << IPI_DDB))
cpu_send_ipi(IPI_DEST_ALL, IPI_DDB);
case IPI_DDB: