--- a/xen/arch/x86/time.c
+++ b/xen/arch/x86/time.c
@@ -578,14 +578,23 @@ static s_time_t __read_platform_stime(u6
     return (stime_platform_stamp + scale_delta(diff, &plt_scale));
 }
 
+#define print_time_scale(prefix, scale, suffix) \
+    printk(prefix "%d:%08x" suffix, (scale)->shift, (scale)->mul_frac);
+
 static void plt_overflow(void *unused)
 {
     int i;
-    u64 count;
-    s_time_t now, plt_now, plt_wrap;
+    u64 count, old_stamp, tsc, pts;
+    s_time_t now, plt_now, plt_wrap, sps;
+    struct time_scale ps;
 
     spin_lock_irq(&platform_timer_lock);
 
+    pts = platform_timer_stamp;
+    sps = stime_platform_stamp;
+    ps = plt_scale;
+
+    old_stamp = plt_stamp;
     count = plt_src.read_counter();
     plt_stamp64 += (count - plt_stamp) & plt_mask;
     plt_stamp = count;
@@ -598,6 +607,19 @@ static void plt_overflow(void *unused)
         plt_wrap = __read_platform_stime(plt_stamp64 + plt_mask + 1);
         if ( ABS(plt_wrap - now) > ABS(plt_now - now) )
             break;
+        rdtscll(tsc);
+        printk("XXX plt_overflow: plt_now=%"PRIx64" plt_wrap=%"PRIx64
+               " now=%"PRIx64" old_stamp=%"PRIx64" new_stamp=%"PRIx64
+               " plt_stamp64=%"PRIx64" plt_mask=%"PRIx64
+               " tsc=%"PRIx64" tsc_stamp=%"PRIx64"\n",
+               plt_now, plt_wrap, now, old_stamp, plt_stamp, plt_stamp64,
+               plt_mask, tsc, this_cpu(cpu_time).local_tsc_stamp);
+        printk("XXX pts=%"PRIx64"/%"PRIx64" sps=%"PRIx64"/%"PRIx64"\n",
+               pts, platform_timer_stamp, sps, stime_platform_stamp);
+        print_time_scale("XXX ps=", &ps, "/");
+        print_time_scale("", &plt_scale, "\n");
+
+        break;
         plt_stamp64 += plt_mask + 1;
     }
     if ( i != 0 )
@@ -694,6 +716,7 @@ static void __init init_platform_timer(v
     plt_mask = (u64)~0ull >> (64 - pts->counter_bits);
 
     set_time_scale(&plt_scale, pts->frequency);
+    print_time_scale("plt_scale=", &plt_scale, "\n");
 
     plt_overflow_period = scale_delta(
         1ull << (pts->counter_bits-1), &plt_scale);