diff --git a/include/benchmark/benchmark.h b/include/benchmark/benchmark.h
index 9182f7a74..7db9f84c6 100644
--- a/include/benchmark/benchmark.h
+++ b/include/benchmark/benchmark.h
@@ -18,13 +18,6 @@
 #include <benchmark/benchmark_tracepoints_types.h>
 #include <mode/hardware.h>
 
-#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
-typedef struct {
-    timestamp_t schedule_start_time;
-    uint64_t    utilisation;
-} benchmark_util_t;
-#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
-
 #if CONFIG_MAX_NUM_TRACE_POINTS > 0
 #define TRACE_POINT_START(x) trace_point_start(x)
 #define TRACE_POINT_STOP(x)   trace_point_stop(x)
diff --git a/include/benchmark/benchmark_utilisation_.h b/include/benchmark/benchmark_utilisation_.h
new file mode 100644
index 000000000..900809e8d
--- /dev/null
+++ b/include/benchmark/benchmark_utilisation_.h
@@ -0,0 +1,26 @@
+/*
+ * Copyright 2016, Data61
+ * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+ * ABN 41 687 119 230.
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(D61_GPL)
+ */
+
+#ifndef _BENCHMARK_UTILISATION_H
+#define _BENCHMARK_UTILISATION_H
+
+#include <config.h>
+#include <arch/benchmark.h>
+
+#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
+typedef struct {
+    timestamp_t schedule_start_time;
+    uint64_t    utilisation;
+} benchmark_util_t;
+#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
+
+#endif /* _BENCHMARK_UTILISATION_H */
diff --git a/include/object/structures.h b/include/object/structures.h
index 909ce7a6a..f3e974fbf 100644
--- a/include/object/structures.h
+++ b/include/object/structures.h
@@ -16,6 +16,7 @@
 #include <stdint.h>
 #include <arch/object/structures_gen.h>
 #include <arch/api/constants.h>
+#include <benchmark/benchmark_utilisation_.h>
 
 enum irq_state {
     IRQInactive  = 0,