diff --git a/repos/base-hw/src/core/kernel/core_interface.h b/repos/base-hw/src/core/kernel/core_interface.h
index a5be22a550..1ea3154e0f 100644
--- a/repos/base-hw/src/core/kernel/core_interface.h
+++ b/repos/base-hw/src/core/kernel/core_interface.h
@@ -68,7 +68,8 @@ namespace Kernel
 	 *
 	 * Kernel and/or hardware may cache parts of a domain configuration. This
 	 * function ensures that the in-memory state of the targeted domain gets
-	 * CPU-locally effective.
+	 * CPU-locally effective. The calling thread must not be destroyed while
+	 * in this syscall.
 	 */
 	inline void update_pd(Pd * const pd)
 	{