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..?".}