> I don't know which method the ARM uses.
With ARM the cache is between the MMU and the CPU. Thus you need to
flush it when the MMU table is changed.
Thus with ARM for high performance you either don't use the MMU or do as
little tasks switches as possible.