diff --git a/include/minix/syslib.h b/include/minix/syslib.h
index dddd916df..70340832c 100755
--- a/include/minix/syslib.h
+++ b/include/minix/syslib.h
@@ -11,6 +11,8 @@
 #include <minix/ipc.h>
 #endif
 
+#include <minix/u64.h>
+
 #ifndef _DEVIO_H
 #include <minix/devio.h>
 #endif
@@ -205,6 +207,9 @@ _PROTOTYPE( int sys_cprof, (int action, int size, int endpt,
                                        void *ctl_ptr, void *mem_ptr)   );
 _PROTOTYPE( int sys_profbuf, (void *ctl_ptr, void *mem_ptr)            );
 
+/* read_tsc() and friends. */
+_PROTOTYPE( void read_tsc_64, (u64_t *t)				);
+_PROTOTYPE( void read_tsc, (u32_t *hi, u32_t *lo)			);
 
 #endif /* _SYSLIB_H */
 
diff --git a/kernel/arch/i386/klib386.s b/kernel/arch/i386/klib386.s
index 04aa8587e..d978c6f52 100755
--- a/kernel/arch/i386/klib386.s
+++ b/kernel/arch/i386/klib386.s
@@ -32,7 +32,6 @@
 .define	_reset		! reset the system
 .define	_idle_task	! task executed when there is no work
 .define	_level0		! call a function at level 0
-.define	_read_tsc	! read the cycle counter (Pentium and up)
 .define	_read_cpu_flags	! read the cpu flags
 .define	_read_cr0	! read cr0
 .define	_write_cr0	! write a value in cr0
@@ -547,24 +546,6 @@ _level0:
 	ret
 
 
-!*===========================================================================*
-!*			      read_tsc					     *
-!*===========================================================================*
-! PUBLIC void read_tsc(unsigned long *high, unsigned long *low);
-! Read the cycle counter of the CPU. Pentium and up. 
-! This function clobbers edx and eax.
-.align 16
-_read_tsc:
-.data1 0x0f		! this is the RDTSC instruction 
-.data1 0x31		! it places the TSC in EDX:EAX
-	push ebp
-	mov ebp, 8(esp)
-	mov (ebp), edx
-	mov ebp, 12(esp)
-	mov (ebp), eax
-	pop ebp
-	ret
-
 !*===========================================================================*
 !*			      read_flags					     *
 !*===========================================================================*
diff --git a/lib/sysutil/Makefile.in b/lib/sysutil/Makefile.in
index c80adaa6d..0443579d4 100644
--- a/lib/sysutil/Makefile.in
+++ b/lib/sysutil/Makefile.in
@@ -18,6 +18,7 @@ libsysutil_FILES=" \
 	report.c \
 	taskcall.c \
 	read_tsc.s \
+	read_tsc_64.c \
 	profile_extern.c \
 	profile.c"
 
diff --git a/lib/sysutil/profile.c b/lib/sysutil/profile.c
index 179de031a..aaa2e5597 100644
--- a/lib/sysutil/profile.c
+++ b/lib/sysutil/profile.c
@@ -20,7 +20,6 @@
 #include <minix/profile.h>
 #include <minix/syslib.h>
 #include <minix/u64.h>
-#include "read_tsc.h"
 
 #define U64_LO 0
 #define U64_HI 1
diff --git a/lib/sysutil/read_tsc.h b/lib/sysutil/read_tsc.h
deleted file mode 100644
index ff72854f8..000000000
--- a/lib/sysutil/read_tsc.h
+++ /dev/null
@@ -1,7 +0,0 @@
-#ifndef READ_TSC_H
-#define READ_TSC_H
-
-_PROTOTYPE(void read_tsc, (unsigned long *hi, unsigned long *lo) );
-
-#endif /* READ_TSC_H */
-
diff --git a/lib/sysutil/read_tsc.s b/lib/sysutil/read_tsc.s
index 5d45b090d..4b8a4d08c 100644
--- a/lib/sysutil/read_tsc.s
+++ b/lib/sysutil/read_tsc.s
@@ -11,13 +11,17 @@
 ! Read the cycle counter of the CPU. Pentium and up. 
 .align 16
 _read_tsc:
+	push edx
+	push eax
 .data1 0x0f		! this is the RDTSC instruction 
 .data1 0x31		! it places the TSC in EDX:EAX
 	push ebp
-	mov ebp, 8(esp)
+	mov ebp, 16(esp)
 	mov (ebp), edx
-	mov ebp, 12(esp)
+	mov ebp, 20(esp)
 	mov (ebp), eax
 	pop ebp
+	pop eax
+	pop edx
 	ret
 
diff --git a/lib/sysutil/read_tsc_64.c b/lib/sysutil/read_tsc_64.c
new file mode 100644
index 000000000..e13ef1ba9
--- /dev/null
+++ b/lib/sysutil/read_tsc_64.c
@@ -0,0 +1,16 @@
+
+#include "sysutil.h"
+#include <minix/u64.h>
+#include <minix/syslib.h>
+
+/* Utility function to work directly with u64_t
+ * By Antonio Mancina
+ */
+PUBLIC void read_tsc_64(t)
+u64_t* t;
+{
+    u32_t lo, hi;
+    read_tsc (&hi, &lo);
+    *t = make64 (lo, hi);
+}
+