Hey Munees, So if you trace from try_init_kernel() (https://github.com/seL4/seL4/blob/master/src/arch/arm/kernel/boot.c#L375), you'll see that on line 375, we do map_kernel_window(). Map_kernel_window() changes the mappings in the kernel's page tables in RAM. But the problem is that the cached TLB mappings in the processor will not be updated to reflect the changes we made, until we invalidate the processor's TLB. So we later on proceed to invalidate the TLB (https://github.com/seL4/seL4/blob/master/src/arch/arm/kernel/boot.c#L222) by calling activate_global_pd() shortly afterward inside of init_cpu(). Activate_global_pd() is a preprocessor macro which is #defined to just resolve down to activate_kernel_vspace (https://github.com/seL4/seL4/blob/master/src/arch/arm/64/kernel/vspace.c#L46...), which is the function in which you are now seeing problems. In short, we need to synchronize the processor's view of the page tables with its TLB caches so that we will be able to see the changes we made to the kernel window. If we don't force those changes to be seen, then we could potentially be accessing the wrong frames in RAM when we are trying to do things like initialize kernel objects and write to device MMIO registers in the kernel. -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO