diff --git a/repos/base-hw/src/core/kernel/thread.cc b/repos/base-hw/src/core/kernel/thread.cc
index d4c6f349a8..fafe75e07f 100644
--- a/repos/base-hw/src/core/kernel/thread.cc
+++ b/repos/base-hw/src/core/kernel/thread.cc
@@ -167,23 +167,27 @@ Tlb_invalidation::Tlb_invalidation(Inter_processor_work_list &global_work_list,
 }
 
 
-Thread::Destroy::Destroy(Thread & caller, Core::Kernel_object<Thread> & to_delete)
+template <typename Obj>
+Thread::Destroy<Obj>::Destroy(Thread &caller, Obj &to_destroy)
 :
-	caller(caller), thread_to_destroy(to_delete)
+	_caller(caller), _obj_to_destroy(to_destroy)
 {
-	thread_to_destroy->_cpu().work_list().insert(&_le);
-	caller._become_inactive(AWAITS_RESTART);
+	_obj_to_destroy->_cpu().work_list().insert(&_le);
+	_caller._become_inactive(AWAITS_RESTART);
 }
 
 
-void
-Thread::Destroy::execute(Cpu &)
+template <typename Obj>
+void Thread::Destroy<Obj>::execute(Cpu &)
 {
-	thread_to_destroy->_cpu().work_list().remove(&_le);
-	thread_to_destroy.destruct();
-	caller._restart();
+	_obj_to_destroy->_cpu().work_list().remove(&_le);
+	_obj_to_destroy.destruct();
+	_caller._restart();
 }
 
+template class Thread::Destroy<Thread>;
+template class Thread::Destroy<Vcpu>;
+
 
 void Thread_fault::print(Genode::Output &out) const
 {
@@ -458,7 +462,7 @@ void Thread::_call_delete_thread()
 	/**
 	 * Construct a cross-cpu work item and send an IPI
 	 */
-	_destroy.construct(*this, to_delete);
+	_thread_destroy.construct(*this, to_delete);
 	to_delete->_cpu().trigger_ip_interrupt();
 }
 
diff --git a/repos/base-hw/src/core/kernel/thread.h b/repos/base-hw/src/core/kernel/thread.h
index ede403f8e2..c7d1fd12f1 100644
--- a/repos/base-hw/src/core/kernel/thread.h
+++ b/repos/base-hw/src/core/kernel/thread.h
@@ -23,6 +23,7 @@
 #include <kernel/inter_processor_work.h>
 #include <kernel/signal.h>
 #include <kernel/ipc_node.h>
+#include <kernel/vcpu.h>
 #include <object.h>
 #include <kernel/interface.h>
 #include <assertion.h>
@@ -97,17 +98,19 @@ class Kernel::Thread : private Kernel::Object, public Cpu_context, private Timeo
 		};
 
 		/**
-		 * The destruction of a thread still active on another cpu
+		 * The destruction of a thread/vcpu still active on another cpu
 		 * needs cross-cpu synchronization
 		 */
+		template <typename OBJ>
 		struct Destroy : Inter_processor_work
 		{
-			using Kthread = Core::Kernel_object<Thread>;
+			using Obj = Core::Kernel_object<OBJ>;
 
-			Thread  & caller; /* the caller gets blocked till the end */
-			Kthread & thread_to_destroy; /* thread to be destroyed */
+			Thread &_caller; /* the caller gets blocked till the end */
+			Obj    &_obj_to_destroy; /* obj to be destroyed */
+
+			Destroy(Thread &caller, Obj &to_destroy);
 
-			Destroy(Thread & caller, Kthread & to_destroy);
 
 			/************************************
 			 ** Inter_processor_work interface **
@@ -144,10 +147,6 @@ class Kernel::Thread : private Kernel::Object, public Cpu_context, private Timeo
 			void execute(Cpu &) override;
 		};
 
-		friend void Tlb_invalidation::execute(Cpu &);
-		friend void Destroy::execute(Cpu &);
-		friend void Flush_and_stop_cpu::execute(Cpu &);
-
 	protected:
 
 		enum { START_VERBOSE = 0 };
@@ -195,7 +194,8 @@ class Kernel::Thread : private Kernel::Object, public Cpu_context, private Timeo
 		Exception_state                    _exception_state          { NO_EXCEPTION };
 
 		Genode::Constructible<Tlb_invalidation>   _tlb_invalidation {};
-		Genode::Constructible<Destroy>            _destroy {};
+		Genode::Constructible<Destroy<Thread>>    _thread_destroy {};
+		Genode::Constructible<Destroy<Vcpu>>      _vcpu_destroy {};
 		Genode::Constructible<Flush_and_stop_cpu> _stop_cpu {};
 
 		/**
diff --git a/repos/base-hw/src/core/kernel/vcpu.h b/repos/base-hw/src/core/kernel/vcpu.h
index 6c97221777..2a1f07959f 100644
--- a/repos/base-hw/src/core/kernel/vcpu.h
+++ b/repos/base-hw/src/core/kernel/vcpu.h
@@ -17,7 +17,6 @@
 #define _CORE__KERNEL__VCPU_H_
 
 /* core includes */
-#include <kernel/cpu.h>
 #include <kernel/cpu_context.h>
 #include <kernel/pd.h>
 #include <kernel/signal.h>
@@ -26,6 +25,9 @@
 
 namespace Kernel {
 
+	class Cpu;
+	class Thread;
+
 	/**
 	 * Kernel backend for a virtual machine
 	 */
@@ -71,6 +73,8 @@ class Kernel::Vcpu : private Kernel::Object, public Cpu_context
 			_scheduled = INACTIVE;
 		}
 
+		friend class Thread;
+
 	public:
 
 		/**
diff --git a/repos/base-hw/src/core/kernel/vcpu_thread_on.cc b/repos/base-hw/src/core/kernel/vcpu_thread_on.cc
index c13a78904a..0d204611d4 100644
--- a/repos/base-hw/src/core/kernel/vcpu_thread_on.cc
+++ b/repos/base-hw/src/core/kernel/vcpu_thread_on.cc
@@ -31,7 +31,27 @@ void Kernel::Thread::_call_new_vcpu()
 }
 
 
-void Kernel::Thread::_call_delete_vcpu() { _call_delete<Vcpu>(); }
+void Kernel::Thread::_call_delete_vcpu()
+{
+	Core::Kernel_object<Vcpu> & to_delete =
+		*(Core::Kernel_object<Vcpu>*)user_arg_1();
+
+	/**
+	 * Delete a vcpu immediately if it is assigned to this cpu,
+	 * or the assigned cpu did not scheduled it.
+	 */
+	if (to_delete->_cpu().id() == Cpu::executing_id() ||
+	    &to_delete->_cpu().current_context() != &*to_delete) {
+		_call_delete<Vcpu>();
+		return;
+	}
+
+	/**
+	 * Construct a cross-cpu work item and send an IPI
+	 */
+	_vcpu_destroy.construct(*this, to_delete);
+	to_delete->_cpu().trigger_ip_interrupt();
+}
 
 
 void Kernel::Thread::_call_run_vcpu()