diff -urpN work.orig/vmmon-only/linux/driver.c work/vmmon-only/linux/driver.c
--- work.orig/vmmon-only/linux/driver.c	2014-04-14 17:06:21.000000000 -0700
+++ work/vmmon-only/linux/driver.c	2014-05-10 18:53:59.266171700 -0700
@@ -1338,7 +1338,7 @@ LinuxDriverReadTSC(void *data,   // OUT:
  *-----------------------------------------------------------------------------
  */
 
-__attribute__((always_inline)) static Bool
+INLINE_SINGLE_CALLER static Bool
 LinuxDriverSyncReadTSCs(uint64 *delta) // OUT: TSC max - TSC min
 {
    TSCDelta tscDelta;