vaale1is
__tlbi(vaale1is, arg);
__flush_s1_tlb_range_op(vaale1is, start, pages, stride, 0,
__tlbi(vaale1is, va);