CTLCPU_CIPI       592 kern/dev/lamebus/lamebus.c 			      CTLCPU_CIPI, 1);
CTLCPU_CIPI       599 kern/dev/lamebus/lamebus.c 			      CTLCPU_CIPI, 0);