I noticed kernel tlbflush.h use tlbi va*, vaa* variants instead of val, vaal ones. Reading the manual D.5.7.2 it appears that va*, vaa* versions invalidate intermediate caching of translation structures. With stage2 enabled that may result in 20+ memory lookups for a 4 level page table walk. That's assuming that intermediate caching structures cache mappings from stage1 table entry to host page. - Mario _______________________________________________ kvmarm mailing list kvmarm@xxxxxxxxxxxxxxxxxxxxx https://lists.cs.columbia.edu/mailman/listinfo/kvmarm