Di seguito un passo di un post di Morsiani chiarificatore sull'interval timer di cui tenere conto anche durante la fase di inizializzazione in initial.c:

Il timer e' un contatore all'indietro che non si ferma mai: conta da p.es. 
0x1000 (valore caricato) a 0, poi 0xFFFFFFFF (-1, ma anche 2^32-1^) 
generando un interrupt nella transizione. 
A ogni context switch lo scheduler, fra le altre cose, deve settare il 
timer per dare un "tot" di tempo di CPU al processo che carica.