2 #include <device/pci.h>
6 wait_for_other_cpus(void)
11 this_processors_id(void)
16 if ((dev = dev_find_slot(0, 0)) == 0)
19 pic1 = pci_read_config32(dev, MPC107_PIC1);
20 return (pic1 & MPC107_PIC1_CF_MP_ID) >> 14;
24 processor_index(unsigned long id)
30 startup_other_cpus(unsigned long *map)