+ // XXX: need to check NOHZ and djw kernel\r
+ diff = (signed int)(us_to - now);\r
+ if (diff > 10000) {\r
+ //printf("sleep %d\n", us_to - now);\r
+ usleep(diff * 15 / 16);\r
+ now = plat_get_ticks_us();\r
+ //printf(" wake %d\n", (signed)(us_to - now));\r
+ }\r
+/*\r
+ while ((signed int)(us_to - now) > 512) {\r