diff -r 675fb031df88 xen/arch/x86/time.c
--- a/xen/arch/x86/time.c	Tue Jul 15 16:13:46 2008 +0100
+++ b/xen/arch/x86/time.c	Tue Jul 15 19:14:16 2008 -0600
@@ -54,14 +54,14 @@ struct cpu_time {
     s_time_t stime_local_stamp;
     s_time_t stime_master_stamp;
     struct time_scale tsc_scale;
-    u64 cstate_plt_count_stamp;
+    u32 cstate_plt_count_stamp;
     struct timer calibration_timer;
 };
 
 struct platform_timesource {
     char *name;
     u64 frequency;
-    u64 (*read_counter)(void);
+    u32 (*read_counter)(void);
     int counter_bits;
 };
 
@@ -340,7 +340,7 @@ static char *freq_string(u64 freq)
  * PLATFORM TIMER 1: PROGRAMMABLE INTERVAL TIMER (LEGACY PIT)
  */
 
-static u64 read_pit_count(void)
+static u32 read_pit_count(void)
 {
     u16 count16;
     u32 count32;
@@ -372,7 +372,7 @@ static void init_pit(struct platform_tim
  * PLATFORM TIMER 2: HIGH PRECISION EVENT TIMER (HPET)
  */
 
-static u64 read_hpet_count(void)
+static u32 read_hpet_count(void)
 {
     return hpet_read32(HPET_COUNTER);
 }
@@ -412,7 +412,7 @@ int use_cyclone;
 /* Cyclone MPMC0 register. */
 static volatile u32 *cyclone_timer;
 
-static u64 read_cyclone_count(void)
+static u32 read_cyclone_count(void)
 {
     return *cyclone_timer;
 }
@@ -462,7 +462,7 @@ u32 pmtmr_ioport;
 /* ACPI PM timer ticks at 3.579545 MHz. */
 #define ACPI_PM_FREQUENCY 3579545
 
-static u64 read_pmtimer_count(void)
+static u32 read_pmtimer_count(void)
 {
     return inl(pmtmr_ioport);
 }
@@ -484,22 +484,15 @@ static int init_pmtimer(struct platform_
  * PLATFORM TIMER 5: TSC
  */
 
-#define platform_timer_is_tsc() (!strcmp(plt_src.name, "TSC"))
+#define platform_timer_is_tsc() (plt_src.counter_bits == 64)
 static u64 tsc_freq;
-
-static u64 read_tsc_count(void)
-{
-    u64 tsc;
-    rdtscll(tsc);
-    return tsc;
-}
 
 static int init_tsctimer(struct platform_timesource *pts)
 {
     /* TODO: evaluate stability of TSC here, return 0 if not stable. */
     pts->name = "TSC";
     pts->frequency = tsc_freq;
-    pts->read_counter = read_tsc_count;
+    pts->read_counter = 0;  /* unused as of now */
     pts->counter_bits = 64;
     return 1;
 }
@@ -518,13 +511,14 @@ static s_time_t stime_platform_stamp; /*
 static s_time_t stime_platform_stamp; /* System time at below platform time */
 static u64 platform_timer_stamp;      /* Platform time at above system time */
 static u64 plt_stamp64;          /* 64-bit platform counter stamp           */
-static u64 plt_stamp;            /* hardware-width platform counter stamp   */
+static u32 plt_stamp;            /* hardware-width platform counter stamp   */
 static struct timer plt_overflow_timer;
 
 static void plt_overflow(void *unused)
 {
-    u64 count;
+    u32 count;
 
+    ASSERT(plt_src.counter_bits != 64);
     spin_lock(&platform_timer_lock);
     count = plt_src.read_counter();
     plt_stamp64 += (count - plt_stamp) & plt_mask;
@@ -536,16 +530,28 @@ static void plt_overflow(void *unused)
 
 static s_time_t __read_platform_stime(u64 platform_time)
 {
-    u64 diff = platform_time - platform_timer_stamp;
+    u64 diff, tsc;
+
+    if ( platform_timer_is_tsc() )
+    {
+        rdtscll(tsc);
+        return scale_delta(tsc, &plt_scale);
+    }
+    diff = platform_time - platform_timer_stamp;
     ASSERT(spin_is_locked(&platform_timer_lock));
     return (stime_platform_stamp + scale_delta(diff, &plt_scale));
 }
 
 static s_time_t read_platform_stime(void)
 {
-    u64 count;
+    u64 count, tsc;
     s_time_t stime;
 
+    if ( platform_timer_is_tsc() )
+    {
+        rdtscll(tsc);
+        return scale_delta(tsc, &plt_scale);
+    }
     spin_lock(&platform_timer_lock);
     count = plt_stamp64 + ((plt_src.read_counter() - plt_stamp) & plt_mask);
     stime = __read_platform_stime(count);
@@ -559,6 +565,8 @@ static void platform_time_calibration(vo
     u64 count;
     s_time_t stamp;
 
+    if ( platform_timer_is_tsc() )
+        return;
     spin_lock(&platform_timer_lock);
     count = plt_stamp64 + ((plt_src.read_counter() - plt_stamp) & plt_mask);
     stamp = __read_platform_stime(count);
@@ -569,6 +577,8 @@ static void platform_time_calibration(vo
 
 static void resume_platform_timer(void)
 {
+    if ( platform_timer_is_tsc() )
+        return;
     /* No change in platform_stime across suspend/resume. */
     platform_timer_stamp = plt_stamp64;
     plt_stamp = plt_src.read_counter();
@@ -604,16 +614,20 @@ static void init_platform_timer(void)
          !init_pmtimer(pts) )
         init_pit(pts);
 
-    plt_mask = (u64)~0ull >> (64 - pts->counter_bits);
-
     set_time_scale(&plt_scale, pts->frequency);
 
-    plt_overflow_period = scale_delta(
-        1ull << (pts->counter_bits-1), &plt_scale);
-    init_timer(&plt_overflow_timer, plt_overflow, NULL, 0);
-    plt_overflow(NULL);
+    if ( !platform_timer_is_tsc() )
+    {
+        plt_mask = (u32)~0u >> (32 - pts->counter_bits);
 
-    platform_timer_stamp = plt_stamp64;
+        plt_overflow_period = scale_delta(
+            1ull << (pts->counter_bits-1), &plt_scale);
+        init_timer(&plt_overflow_timer, plt_overflow, NULL, 0);
+        plt_overflow(NULL);
+
+        platform_timer_stamp = plt_stamp64;
+    }
+
 
     printk("Platform timer is %s %s\n",
            freq_string(pts->frequency), pts->name);
@@ -633,9 +647,10 @@ void cstate_restore_tsc(void)
 void cstate_restore_tsc(void)
 {
     struct cpu_time *t = &this_cpu(cpu_time);
-    u64 plt_count_delta, tsc_delta;
+    u32    plt_count_delta;
+    u64    tsc_delta;
 
-    if ( tsc_invariant )
+    if ( tsc_invariant || platform_timer_is_tsc() )
         return;
 
     plt_count_delta = (plt_src.read_counter() -
@@ -736,14 +751,18 @@ static unsigned long get_cmos_time(void)
 
 s_time_t get_s_time(void)
 {
-    struct cpu_time *t = &this_cpu(cpu_time);
+    struct cpu_time *t;
     u64 tsc, delta;
     s_time_t now;
 
     rdtscll(tsc);
-    delta = tsc - t->local_tsc_stamp;
-    now = t->stime_local_stamp + scale_delta(delta, &t->tsc_scale);
-
+    if ( platform_timer_is_tsc() )
+        now = scale_delta(tsc, &plt_scale);
+    else {
+        t = &this_cpu(cpu_time);
+        delta = tsc - t->local_tsc_stamp;
+        now = t->stime_local_stamp + scale_delta(delta, &t->tsc_scale);
+    }
     return now;
 }
 
@@ -1008,12 +1027,9 @@ void init_percpu_time(void)
     unsigned long flags;
     s_time_t now;
 
-    if ( platform_timer_is_tsc() )
-        return;
-
     local_irq_save(flags);
     rdtscll(t->local_tsc_stamp);
-    now = read_platform_stime();
+    now = !plt_src.read_counter ? 0 : read_platform_stime();
     local_irq_restore(flags);
 
     t->stime_master_stamp = now;
@@ -1031,10 +1047,10 @@ int __init init_xen_time(void)
 
     local_irq_disable();
 
+    init_percpu_time();
+
     stime_platform_stamp = 0;
     init_platform_timer();
-
-    init_percpu_time();
 
     /* check if TSC is invariant during deep C state
        this is a new feature introduced by Nehalem*/