Just to finish off the discussion, the timer hardware that neutrino uses to generate the tick is up to the BSP developer
. On a PPC600 family chip, it's _usually_ the decrementer, but doesn't need to be.  The kernel controls the hardware via
 the timer_load/timer_reload/timer_value callout functions in the qtime section of the system page.

In any case, the Interrupt[Lock/Disable] function is expected to turn off all interrupt sources.