diff -r eb71d05f51a2 xen/arch/x86/setup.c
--- a/xen/arch/x86/setup.c	Mon Jul 28 11:43:54 2008 +0100
+++ b/xen/arch/x86/setup.c	Mon Jul 28 10:47:11 2008 -0600
@@ -944,14 +944,6 @@ void __init __start_xen(unsigned long mb
 
     smp_prepare_cpus(max_cpus);
 
-    /*
-     * Initialise higher-level timer functions. We do this fairly late
-     * (post-SMP) because the time bases and scale factors need to be updated 
-     * regularly, and SMP initialisation can cause a long delay with 
-     * interrupts not yet enabled.
-     */
-    init_xen_time();
-
     initialize_keytable();
 
     serial_init_postirq();
@@ -976,6 +968,14 @@ void __init __start_xen(unsigned long mb
 
     printk("Brought up %ld CPUs\n", (long)num_online_cpus());
     smp_cpus_done(max_cpus);
+
+    /*
+     * Initialise higher-level timer functions. We do this fairly late
+     * (post-SMP) because the time bases and scale factors need to be updated 
+     * regularly, and SMP initialisation can cause a long delay with 
+     * interrupts not yet enabled.
+     */
+    init_xen_time();
 
     initialise_gdb(); /* could be moved earlier */
 
diff -r eb71d05f51a2 xen/arch/x86/time.c
--- a/xen/arch/x86/time.c	Mon Jul 28 11:43:54 2008 +0100
+++ b/xen/arch/x86/time.c	Mon Jul 28 10:47:11 2008 -0600
@@ -752,6 +752,9 @@ static unsigned long get_cmos_time(void)
  * System Time
  ***************************************************************************/
 
+u32 stime_minstep = 0;
+static DEFINE_SPINLOCK(stime_lock);
+
 s_time_t get_s_time(void)
 {
     struct cpu_time *t = &this_cpu(cpu_time);
@@ -763,6 +766,41 @@ s_time_t get_s_time(void)
     now = t->stime_local_stamp + scale_delta(delta, &t->tsc_scale);
 
     return now;
+}
+
+/* monotonically increasing stime is required because of inter-CPU skew */
+s_time_t get_s_time_mono(void)
+{
+    s_time_t now;
+    unsigned long flags;
+    static s_time_t last = 0;
+
+    spin_lock_irqsave(&stime_lock, flags);
+    now = get_s_time();
+    if ( (int64_t)(now - last) >= 0 )
+        last = now;
+    else
+        now = (last += stime_minstep);
+    spin_unlock_irqrestore(&stime_lock, flags);
+
+    return now;
+}
+
+void init_stime_resolution(void)
+{
+    u32 dif, minstep = 0xffffffff;
+    int i, ncpus = num_online_cpus();
+    s_time_t t1, t2;
+
+    for (i = 0; i < 10; i++)
+    {
+        t1 = get_s_time_mono();
+        t2 = get_s_time_mono();
+        dif = t2 - t1;
+        if (dif < minstep)
+            minstep = dif;
+    }
+    stime_minstep = minstep / ncpus;
 }
 
 static inline void version_update_begin(u32 *version)
@@ -1069,6 +1107,8 @@ int __init init_xen_time(void)
     stime_platform_stamp = 0;
     init_platform_timer();
 
+    init_stime_resolution();
+
     do_settime(get_cmos_time(), 0, NOW());
 
     local_irq_enable();