2 files changed, 2 insertions, 2 deletions
diff --git a/pk/frontend.c b/pk/frontend.c
index fa5db51..1cb99db 100644
--- a/pk/frontend.c
+++ b/pk/frontend.c
@@ -17,8 +17,7 @@ sysret_t frontend_syscall(long n, long a0, long a1, long a2, long a3)
   magic_mem[3] = a2;
   magic_mem[4] = a3;
 
-  asm volatile ("fence");
-  asm volatile ("cflush");
+  asm volatile ("cflush; fence");
 
   mtpcr(magic_mem,PCR_TOHOST);
   while(mfpcr(PCR_FROMHOST) == 0);
diff --git a/pk/pk.c b/pk/pk.c
index 9c6653d..a0c4ecb 100644
--- a/pk/pk.c
+++ b/pk/pk.c
@@ -162,6 +162,7 @@ static void jump_usrstart(const char* fn)
 
   int user64;
   long start = load_elf(fn, &user64);
+  asm volatile("cflush; fence");
   init_tf(&tf, start, USER_MEM_SIZE-USER_MAINVARS_SIZE, user64);
   pop_tf(&tf);
 }