2 files changed, 10 insertions, 1 deletions
diff --git a/machine/flush_icache.h b/machine/flush_icache.h
new file mode 100644
index 0000000..92166bc
--- /dev/null
+++ b/machine/flush_icache.h
@@ -0,0 +1,8 @@
+// See LICENSE for license details.
+
+#ifndef _RISCV_FLUSH_ICACHE_H
+#define _RISCV_FLUSH_ICACHE_H
+
+void __riscv_flush_icache(void);
+
+#endif /* _RISCV_FLUSH_ICACHE_H */
diff --git a/pk/pk.c b/pk/pk.c
index 4f16abc..b8c9337 100644
--- a/pk/pk.c
+++ b/pk/pk.c
@@ -8,6 +8,7 @@
 #include "frontend.h"
 #include "bits.h"
 #include "usermem.h"
+#include "flush_icache.h"
 #include <stdbool.h>
 
 elf_info current;
@@ -174,7 +175,7 @@ static void run_loaded_program(size_t argc, char** argv, uintptr_t kstack_top)
 
   trapframe_t tf;
   init_tf(&tf, current.entry, stack_top);
-  __clear_cache(0, 0);
+  __riscv_flush_icache();
   write_csr(sscratch, kstack_top);
   start_user(&tf);
 }