* restart. This yields a free running counter guaranteed to take almost 6
  * years to wrap around even at 100GHz clock rate.
  */
-u64 __attribute__((no_instrument_function)) get_ticks(void)
+u64 notrace get_ticks(void)
 {
        u64 now_tick = rdtsc();
 
 }
 
 /* Get the speed of the TSC timer in MHz */
-unsigned __attribute__((no_instrument_function)) long get_tbclk_mhz(void)
+unsigned notrace long get_tbclk_mhz(void)
 {
        unsigned long fast_calibrate;
 
        return get_ms_timer() - base;
 }
 
-ulong __attribute__((no_instrument_function)) timer_get_us(void)
+ulong notrace timer_get_us(void)
 {
        return get_ticks() / get_tbclk_mhz();
 }