diff --git a/include/arch/x86/arch/64/mode/fastpath/fastpath.h b/include/arch/x86/arch/64/mode/fastpath/fastpath.h
index 90c356c73..f4489c4d4 100644
--- a/include/arch/x86/arch/64/mode/fastpath/fastpath.h
+++ b/include/arch/x86/arch/64/mode/fastpath/fastpath.h
@@ -94,6 +94,8 @@ fastpath_mi_check(word_t msgInfo)
 static inline void NORETURN
 fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread)
 {
+    c_exit_hook();
+
     if (unlikely(cur_thread == x86KSfpuOwner)) {
         /* We are using the FPU, make sure it is enabled */
         enableFpu();