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[..]".