#include unsigned int tsc = tsc_khz;