apic_send_ipi
apic_send_ipi,
void apic_send_ipi(int, int);
extern void apic_send_ipi(int cpun, int ipl);