diff -r 8afcb103a82e -r d879a42f78c4 src/arch/x86/utility.cc
--- a/src/arch/x86/utility.cc	Mon Jun 03 14:30:31 2013 +0200
+++ b/src/arch/x86/utility.cc	Mon Jun 03 14:31:18 2013 +0200
@@ -209,6 +209,10 @@
         dest->setMiscRegNoEffect(i, src->readMiscRegNoEffect(i));
     }
 
+    // The TSC has to be updated with side-effects if the CPUs in a
+    // CPU switch have different frequencies.
+    dest->setMiscReg(MISCREG_TSC, src->readMiscReg(MISCREG_TSC));
+
     dest->getITBPtr()->flushAll();
     dest->getDTBPtr()->flushAll();
 }