uint32_t generation;
int cpu;
#ifdef __i386__
sched_pin();
#endif
/*
* It is not necessary to signal other CPUs while booting or
* when in the debugger.