diff --git a/include/benchmark/benchmark.h b/include/benchmark/benchmark.h
index 7db9f84c6..91d57d602 100644
--- a/include/benchmark/benchmark.h
+++ b/include/benchmark/benchmark.h
@@ -27,8 +27,8 @@
 extern timestamp_t ksEntries[CONFIG_MAX_NUM_TRACE_POINTS];
 extern bool_t ksStarted[CONFIG_MAX_NUM_TRACE_POINTS];
 extern timestamp_t ksExit;
-extern uint32_t ksLogIndex;
-extern uint32_t ksLogIndexFinalized;
+extern seL4_Word ksLogIndex;
+extern seL4_Word ksLogIndexFinalized;
 extern paddr_t ksUserLogBuffer;
 
 static inline void
diff --git a/include/benchmark/benchmark_track.h b/include/benchmark/benchmark_track.h
index ff10edd06..1dbc125a3 100644
--- a/include/benchmark/benchmark_track.h
+++ b/include/benchmark/benchmark_track.h
@@ -33,8 +33,8 @@ extern kernel_entry_t ksKernelEntry;
              sizeof(benchmark_track_kernel_entry_t))
 
 extern timestamp_t ksEnter;
-extern word_t ksLogIndex;
-extern uint32_t ksLogIndexFinalized;
+extern seL4_Word ksLogIndex;
+extern seL4_Word ksLogIndexFinalized;
 
 /**
  * @brief Fill in logging info for kernel entries