Index: linux-2.6/drivers/kvm/svm.c
===================================================================
--- linux-2.6.orig/drivers/kvm/svm.c	2007-03-02 17:29:57.000000000 +0200
+++ linux-2.6/drivers/kvm/svm.c	2007-03-02 17:31:15.000000000 +0200
@@ -598,9 +598,45 @@
 	kfree(vcpu->svm);
 }
 
+#ifdef CONFIG_SMP
+static void ipi_rdtscll(void *arg)
+{
+	u64 *tsc = arg;
+	rdtscll(*tsc);
+}
+#endif
+
+/*
+ * Switches to specified vcpu, until a matching vcpu_put(), but assumes
+ * vcpu mutex is already taken.
+ */
 static struct kvm_vcpu *svm_vcpu_load(struct kvm_vcpu *vcpu)
 {
-	get_cpu();
+	int cpu;
+
+	cpu = get_cpu();
+
+#ifdef CONFIG_SMP
+	if (vcpu->cpu != cpu) {
+		if (vcpu->cpu != -1) {
+			u64 tsc_this, tsc_previous;
+
+			/* Get TSC value for this and the previous cpu. */
+			rdtscll(tsc_this);
+			smp_call_function_single(vcpu->cpu, ipi_rdtscll,
+						 &tsc_previous, 0, 1);
+
+			/*
+			 * Make sure that the guest sees a monotonically
+			 * increasing TSC.
+			 */
+			vcpu->svm->vmcb->control.tsc_offset +=
+						tsc_previous - tsc_this;
+		}
+	}
+#endif
+
+	vcpu->cpu = cpu;
 	return vcpu;
 }
 
Index: linux-2.6/drivers/kvm/vmx.c
===================================================================
--- linux-2.6.orig/drivers/kvm/vmx.c	2007-03-02 17:30:01.000000000 +0200
+++ linux-2.6/drivers/kvm/vmx.c	2007-03-02 17:30:17.000000000 +0200
@@ -200,6 +200,14 @@
 #endif
 }
 
+#ifdef CONFIG_SMP
+static void ipi_rdtscll(void *arg)
+{
+	u64 *tsc = arg;
+	rdtscll(*tsc);
+}
+#endif
+
 /*
  * Switches to specified vcpu, until a matching vcpu_put(), but assumes
  * vcpu mutex is already taken.
@@ -230,6 +238,25 @@
 		struct descriptor_table dt;
 		unsigned long sysenter_esp;
 
+#ifdef CONFIG_SMP
+		if (vcpu->cpu != -1) {
+			u64 tsc_this, tsc_previous, guest_tsc_offset;
+
+			/* Get TSC value for this and the previous cpu. */
+			rdtscll(tsc_this);
+			smp_call_function_single(vcpu->cpu, ipi_rdtscll,
+						 &tsc_previous, 0, 1);
+
+			/*
+			 * Make sure that the guest sees a monotonically
+			 * increasing TSC.
+			 */
+			guest_tsc_offset = vmcs_read64(TSC_OFFSET);
+			vmcs_write64(TSC_OFFSET, guest_tsc_offset +
+				     		tsc_previous - tsc_this);
+		}
+#endif
+
 		vcpu->cpu = cpu;
 		/*
 		 * Linux uses per-cpu TSS and GDT, so set these when switching