diff --git a/kernel/sched/core.c b/kernel/sched/core.c
index 34e2291a9a6c163be3dfd774ed110bf07ab0e890..e1ae6ac15eac94bb6562cb8d206190ec60a9cd5f 100644
--- a/kernel/sched/core.c
+++ b/kernel/sched/core.c
@@ -23,6 +23,9 @@
 
 #include <asm/switch_to.h>
 #include <asm/tlb.h>
+#ifdef CONFIG_PARAVIRT
+#include <asm/paravirt.h>
+#endif
 
 #include "sched.h"
 #include "../workqueue_internal.h"