diff -r 08f77df14cba xen/arch/x86/hvm/vpt.c
--- a/xen/arch/x86/hvm/vpt.c	Wed Jul 02 11:30:37 2008 +0900
+++ b/xen/arch/x86/hvm/vpt.c	Wed Jul 02 16:34:33 2008 -0600
@@ -47,7 +47,7 @@ u64 hvm_get_guest_time(struct vcpu *v)
     if ( (int64_t)(now - pl->last_guest_time) >= 0 )
         pl->last_guest_time = now;
     else
-        now = pl->last_guest_time;
+        now = ++pl->last_guest_time;
     spin_unlock(&pl->pl_time_lock);
 
     return now + v->arch.hvm_vcpu.stime_offset;
diff -r 08f77df14cba xen/arch/x86/time.c
--- a/xen/arch/x86/time.c	Wed Jul 02 11:30:37 2008 +0900
+++ b/xen/arch/x86/time.c	Wed Jul 02 16:34:33 2008 -0600
@@ -69,6 +69,9 @@ static DEFINE_PER_CPU(struct cpu_time, c
 
 /* TSC is invariant on C state entry? */
 static bool_t tsc_invariant;
+
+/* record maximum skew to report with debug-key t */
+u64 max_stime_skew = 0;
 
 /*
  * We simulate a 32-bit platform timer from the 16-bit PIT ch2 counter.
@@ -845,6 +848,23 @@ static void local_time_calibration(void 
     rdtscll(curr_tsc);
     local_irq_enable();
 
+    /*
+     * Record maximum stime skew from master processor.  Note that
+     * in the case of a fast local clock, skew reflects the post-adjusted
+     * skew (see below and get_s_time()), not the actual skew.  Also
+     * note that some processors may skew positive and others negative
+     * relative to master so skew between ANY pair of processors may be
+     * as much as 2x recorded max
+     */
+    if ( smp_processor_id() )
+    {
+        s64 curr_stime_skew = curr_master_stime - curr_local_stime;
+        if ( curr_stime_skew < 0 )
+            curr_stime_skew = - curr_stime_skew;
+        if ( curr_stime_skew > max_stime_skew )
+            max_stime_skew = curr_stime_skew;
+    }
+
 #if 0
     printk("PRE%d: tsc=%"PRIu64" stime=%"PRIu64" master=%"PRIu64"\n",
            smp_processor_id(), prev_tsc, prev_local_stime, prev_master_stime);
diff -r 08f77df14cba xen/common/keyhandler.c
--- a/xen/common/keyhandler.c	Wed Jul 02 11:30:37 2008 +0900
+++ b/xen/common/keyhandler.c	Wed Jul 02 16:34:33 2008 -0600
@@ -251,6 +251,7 @@ static void read_clocks(unsigned char ke
     unsigned int cpu = smp_processor_id(), min_cpu, max_cpu;
     u64 min, max, dif, difus;
     static DEFINE_SPINLOCK(lock);
+    extern u64 max_stime_skew;
 
     spin_lock(&lock);
 
@@ -284,6 +285,7 @@ static void read_clocks(unsigned char ke
     printk("Min = %"PRIu64" ; Max = %"PRIu64" ; Diff = %"PRIu64
            " (%"PRIu64" microseconds)\n",
            min, max, dif, difus);
+    printk("Max recorded stime skew = %"PRIu64"ns\n", max_stime_skew);
 }
 
 extern void dump_runq(unsigned char key);