diff --git a/libsel4/arch_include/arm/sel4/arch/syscalls.h b/libsel4/arch_include/arm/sel4/arch/syscalls.h
index 820b086e5..1a1dd6c3b 100644
--- a/libsel4/arch_include/arm/sel4/arch/syscalls.h
+++ b/libsel4/arch_include/arm/sel4/arch/syscalls.h
@@ -391,11 +391,18 @@ seL4_BenchmarkResetLog(void)
     return (seL4_Error) ret;
 }
 
-LIBSEL4_INLINE_FUNC void
+LIBSEL4_INLINE_FUNC seL4_Word
 seL4_BenchmarkFinalizeLog(void)
 {
-    arm_sys_null(seL4_SysBenchmarkFinalizeLog);
-    asm volatile("" ::: "memory");
+    seL4_Word unused0 = 0;
+    seL4_Word unused1 = 0;
+    seL4_Word unused2 = 0;
+    seL4_Word unused3 = 0;
+    seL4_Word unused4 = 0;
+    seL4_Word index_ret;
+    arm_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
+
+    return (seL4_Word)index_ret;
 }
 
 LIBSEL4_INLINE_FUNC seL4_Error
diff --git a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
index 1363f5058..247439c55 100644
--- a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
+++ b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
@@ -603,11 +603,16 @@ seL4_BenchmarkResetLog(void)
     return (seL4_Error)ret;
 }
 
-LIBSEL4_INLINE_FUNC void
+LIBSEL4_INLINE_FUNC seL4_Word
 seL4_BenchmarkFinalizeLog(void)
 {
-    x86_sys_null(seL4_SysBenchmarkFinalizeLog);
-    asm volatile("" :::"%esi", "%edi", "memory");
+    seL4_Word unused0 = 0;
+    seL4_Word unused1 = 0;
+    seL4_Word unused2 = 0;
+    seL4_Word index_ret;
+    x86_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2);
+
+    return (seL4_Word)index_ret;
 }
 
 LIBSEL4_INLINE_FUNC seL4_Error
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
index 3302461ea..4ee9e8750 100644
--- a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
@@ -419,11 +419,18 @@ seL4_BenchmarkResetLog(void)
     return (seL4_Error)ret;
 }
 
-LIBSEL4_INLINE_FUNC void
+LIBSEL4_INLINE_FUNC seL4_Word
 seL4_BenchmarkFinalizeLog(void)
 {
-    x64_sys_null(seL4_SysBenchmarkFinalizeLog);
-    asm volatile("" ::: "memory");
+    seL4_Word unused0 = 0;
+    seL4_Word unused1 = 0;
+    seL4_Word unused2 = 0;
+    seL4_Word unused3 = 0;
+    seL4_Word unused4 = 0;
+    seL4_Word index_ret;
+    x64_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
+
+    return (seL4_Word)index_ret;
 }
 
 LIBSEL4_INLINE_FUNC seL4_Error
diff --git a/src/api/syscall.c b/src/api/syscall.c
index 236ef3812..9d2cb80e6 100644
--- a/src/api/syscall.c
+++ b/src/api/syscall.c
@@ -147,6 +147,7 @@ handleUnknownSyscall(word_t w)
     } else if (w == SysBenchmarkFinalizeLog) {
 #ifdef CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER
         ksLogIndexFinalized = ksLogIndex;
+        setRegister(NODE_STATE(ksCurThread), capRegister, ksLogIndexFinalized);
 #endif /* CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER */
 #ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
         benchmark_utilisation_finalise();
diff --git a/src/arch/arm/benchmark/benchmark.c b/src/arch/arm/benchmark/benchmark.c
index 0eeb0be69..846671ab9 100644
--- a/src/arch/arm/benchmark/benchmark.c
+++ b/src/arch/arm/benchmark/benchmark.c
@@ -16,9 +16,7 @@
 timestamp_t ksEntries[CONFIG_MAX_NUM_TRACE_POINTS];
 bool_t ksStarted[CONFIG_MAX_NUM_TRACE_POINTS];
 timestamp_t ksExit;
-uint32_t ksLogIndex = 0;
-uint32_t ksLogIndexFinalized = 0;
+seL4_Word ksLogIndex = 0;
+seL4_Word ksLogIndexFinalized = 0;
 
 #endif /* CONFIG_MAX_NUM_TRACE_POINTS > 0 */
-
-
diff --git a/src/arch/x86/benchmark/benchmark.c b/src/arch/x86/benchmark/benchmark.c
index a42fdec17..8108cd096 100644
--- a/src/arch/x86/benchmark/benchmark.c
+++ b/src/arch/x86/benchmark/benchmark.c
@@ -17,8 +17,7 @@
 timestamp_t ksEntries[CONFIG_MAX_NUM_TRACE_POINTS];
 bool_t ksStarted[CONFIG_MAX_NUM_TRACE_POINTS];
 timestamp_t ksExit;
-uint32_t ksLogIndex = 0;
-uint32_t ksLogIndexFinalized = 0;
+seL4_Word ksLogIndex = 0;
+seL4_Word ksLogIndexFinalized = 0;
 
 #endif /* CONFIG_MAX_NUM_TRACE_POINTS > 0 */
-
diff --git a/src/benchmark/benchmark_track.c b/src/benchmark/benchmark_track.c
index 62a7231df..37bb726b0 100644
--- a/src/benchmark/benchmark_track.c
+++ b/src/benchmark/benchmark_track.c
@@ -15,8 +15,8 @@
 #ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES
 
 timestamp_t ksEnter;
-word_t ksLogIndex;
-uint32_t ksLogIndexFinalized;
+seL4_Word ksLogIndex;
+seL4_Word ksLogIndexFinalized;
 
 void benchmark_track_exit(void)
 {