stickintr
int stickintr(void *); /* system tick interrupt code */
stickintr_establish(PIL_CLOCK, stickintr);