properly with HZ != 100, causing tb_to_us to be wrong and gettimeofday()
to return strangely "off" results