diff --git a/apps/sel4bench/src/plat/pc99/plat.c b/apps/sel4bench/src/plat/pc99/plat.c
index 265e5855..fe24a377 100644
--- a/apps/sel4bench/src/plat/pc99/plat.c
+++ b/apps/sel4bench/src/plat/pc99/plat.c
@@ -7,10 +7,4 @@
 
 void plat_setup(env_t *env)
 {
-    if (config_set(CONFIG_ARCH_X86_64)) {
-        /* check if the cpu supports rdtscp */
-        int edx = 0;
-        asm volatile("cpuid":"=d"(edx):"a"(0x80000001):"ecx");
-        ZF_LOGF_IF((edx & (BIT(27))) == 0, "CPU does not support rdtscp instruction");
-    }
 }
diff --git a/libsel4benchsupport/sel4_arch_include/x86_64/sel4_arch/ipc.h b/libsel4benchsupport/sel4_arch_include/x86_64/sel4_arch/ipc.h
index b78a922d..73a211d2 100644
--- a/libsel4benchsupport/sel4_arch_include/x86_64/sel4_arch/ipc.h
+++ b/libsel4benchsupport/sel4_arch_include/x86_64/sel4_arch/ipc.h
@@ -162,31 +162,8 @@
 } while (0)
 #endif /* CONFIG_KERNEL_MCS */
 
-#define READ_COUNTER_BEFORE(var) do { \
-    uint32_t low, high; \
-    asm volatile( \
-            "cpuid \n" \
-            "rdtsc \n" \
-            "movl %%edx, %0 \n" \
-            "movl %%eax, %1 \n" \
-            : "=r"(high), "=r"(low) \
-            : \
-            : "%rax", "%rbx", "%rcx", "%rdx"); \
-    (var) = (((uint64_t)high) << 32ull) | ((uint64_t)low); \
-} while (0)
-
-#define READ_COUNTER_AFTER(var) do { \
-    uint32_t low, high; \
-    asm volatile( \
-            "rdtscp \n" \
-            "movl %%edx, %0 \n" \
-            "movl %%eax, %1 \n" \
-            "cpuid \n" \
-            : "=r"(high), "=r"(low) \
-            : \
-            : "%rax", "rbx", "%rcx", "%rdx"); \
-    (var) = (((uint64_t)high) << 32ull) | ((uint64_t)low); \
-} while (0)
+#define READ_COUNTER_BEFORE SEL4BENCH_READ_CCNT
+#define READ_COUNTER_AFTER  SEL4BENCH_READ_CCNT
 
 #define DO_REAL_CALL(ep, tag) DO_CALL(ep, tag, "syscall")
 #define DO_NOP_CALL(ep, tag) DO_CALL(ep, tag, ".byte 0x66\n.byte 0x90")