diff --git a/include/arch/arm/arch/object/vcpu.h b/include/arch/arm/arch/object/vcpu.h
index fb45fe976..63044d48f 100644
--- a/include/arch/arm/arch/object/vcpu.h
+++ b/include/arch/arm/arch/object/vcpu.h
@@ -124,6 +124,7 @@ exception_t decodeARMVCPUInvocation(
 void vcpu_restore(vcpu_t *cpu);
 void vcpu_switch(vcpu_t *cpu);
 void vcpu_flush(void);
+void vcpu_flush_if_current(tcb_t *tptr);
 #ifdef ENABLE_SMP_SUPPORT
 void handleVCPUInjectInterruptIPI(vcpu_t *vcpu, unsigned long index, virq_t virq);
 #endif /* ENABLE_SMP_SUPPORT */
@@ -208,6 +209,7 @@ static inline VPPIEventIRQ_t irqVPPIEventIndex(irq_t irq)
 #define vcpu_boot_init() do {} while(0)
 #define vcpu_switch(x) do {} while(0)
 #define vcpu_flush() do {} while(0)
+#define vcpu_flush_if_current(x) do {} while(0)
 static inline void VGICMaintenance(void) {}
 
 #endif /* end of !CONFIG_ARM_HYPERVISOR_SUPPORT */
diff --git a/include/kernel/thread.h b/include/kernel/thread.h
index 475195482..4a828f6bc 100644
--- a/include/kernel/thread.h
+++ b/include/kernel/thread.h
@@ -165,6 +165,7 @@ void Arch_switchToIdleThread(void);
 void Arch_configureIdleThread(tcb_t *tcb);
 void Arch_activateIdleThread(tcb_t *tcb);
 void Arch_prepareNextDomain(void);
+void Arch_prepareSetDomain(tcb_t *tcb, dom_t dom);
 
 void NORETURN idle_thread(void);
 
diff --git a/src/arch/arm/kernel/thread.c b/src/arch/arm/kernel/thread.c
index 5dd4c1f20..713cba492 100644
--- a/src/arch/arm/kernel/thread.c
+++ b/src/arch/arm/kernel/thread.c
@@ -17,3 +17,10 @@ void Arch_prepareNextDomain(void)
         vcpu_flush();
     }
 }
+
+void Arch_prepareSetDomain(tcb_t *tptr, dom_t dom)
+{
+    if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
+        vcpu_flush_if_current(tptr);
+    }
+}
diff --git a/src/arch/arm/object/vcpu.c b/src/arch/arm/object/vcpu.c
index 7a86fbc66..673a254b7 100644
--- a/src/arch/arm/object/vcpu.c
+++ b/src/arch/arm/object/vcpu.c
@@ -272,6 +272,13 @@ void vcpu_flush(void)
     }
 }
 
+void vcpu_flush_if_current(tcb_t *tptr)
+{
+    if (tptr->tcbArch.tcbVCPU == ARCH_NODE_STATE(armHSCurVCPU)) {
+        vcpu_flush();
+    }
+}
+
 void vcpu_finalise(vcpu_t *vcpu)
 {
     if (vcpu->vcpuTCB) {
diff --git a/src/arch/riscv/kernel/thread.c b/src/arch/riscv/kernel/thread.c
index a2239a593..5502681b6 100644
--- a/src/arch/riscv/kernel/thread.c
+++ b/src/arch/riscv/kernel/thread.c
@@ -60,3 +60,8 @@ void Arch_prepareNextDomain(void)
 {
     /* Don't need to do anything */
 }
+
+void Arch_prepareSetDomain(tcb_t *tptr, dom_t dom)
+{
+    /* Don't need to do anything */
+}
diff --git a/src/arch/x86/kernel/thread.c b/src/arch/x86/kernel/thread.c
index 28e50aefe..580029b40 100644
--- a/src/arch/x86/kernel/thread.c
+++ b/src/arch/x86/kernel/thread.c
@@ -16,3 +16,8 @@ void Arch_prepareNextDomain(void)
 {
     /* Don't need to do anything */
 }
+
+void Arch_prepareSetDomain(tcb_t *tptr, dom_t dom)
+{
+    /* Don't need to do anything */
+}
diff --git a/src/kernel/thread.c b/src/kernel/thread.c
index 3fc32f15a..d6fc2d85e 100644
--- a/src/kernel/thread.c
+++ b/src/kernel/thread.c
@@ -304,12 +304,13 @@ void doNBRecvFailedTransfer(tcb_t *thread)
 
 void prepareSetDomain(tcb_t *tptr, dom_t dom)
 {
-#ifdef CONFIG_HAVE_FPU
     if (ksCurDomain != dom) {
+        Arch_prepareSetDomain(tptr, dom);
+#ifdef CONFIG_HAVE_FPU
         /* Save FPU state now to avoid touching cross-domain state later */
         fpuRelease(tptr);
-    }
 #endif
+    }
 }
 
 static void prepareNextDomain(void)