According to Section D5.10.3 "Maintenance requirements on changing System
register values" of the architecture manual, an isb instruction should be
executed after updating ttbr0_el1 and before invalidating the TLB.