diff -urN cgl-1408/arch/x86_64/kernel/time.c cgl-1408-tsc/arch/x86_64/kernel/time.c
--- cgl-1408/arch/x86_64/kernel/time.c	2003-08-14 02:54:04.000000000 +0200
+++ cgl-1408-tsc/arch/x86_64/kernel/time.c	2003-08-15 09:48:11.000000000 +0200
@@ -55,6 +55,7 @@
 {
 	unsigned long t;
 	rdtscll_sync(&t);	
+	if (t < vxtime.last_tsc) t = vxtime.last_tsc;
 	return ((t  - vxtime.last_tsc) * vxtime.tsc_quot) >> 32;
 }
 
diff -urN cgl-1408/arch/x86_64/kernel/vsyscall.c cgl-1408-tsc/arch/x86_64/kernel/vsyscall.c
--- cgl-1408/arch/x86_64/kernel/vsyscall.c	2003-08-14 02:54:02.000000000 +0200
+++ cgl-1408-tsc/arch/x86_64/kernel/vsyscall.c	2003-08-15 09:47:05.000000000 +0200
@@ -72,6 +72,7 @@
 			case VXTIME_TSC:
 				sync_core();
 				rdtscll(t);
+				if (t < __vxtime.last_tsc) t = __vxtime.last_tsc;
 				usec += (((t  - __vxtime.last_tsc) * __vxtime.tsc_quot) >> 32);
 				break;