Per my understanding, "isb" and "dsb" do not flush TLB. "isb" has the effect of flushling pipeline.

Roughly, "dsb" ensures that memory accesses and some TLB/cache maintenance instructions are completed before executing the instructions after "dsb". These opeartions may depend on the value of TTBR0_EL1. Also, if I remeber correctly, "isb" should be used after modifying a control register so that the modification can be observed by the instructions following the instruction that modifies the control register, through the effect of flushing pipeline and refetching instructions.

From: Devel <devel-bounces@sel4.systems> on behalf of Dd Nirvana <ddnirvana1@gmail.com>
Sent: Saturday, December 1, 2018 7:23 PM
To: devel@sel4.systems
Subject: [seL4] Is the ASID used in seL4 by default?

Hi guys,

I found that seL4's ARM version still need "isb" and "dsb" around updating TTBR0_EL1.

This fence will flush the TLB and will affect IPC performance. However, it seems that enabling ASID can avoid this costs.

I am not sure, is there any concern that makes seL4 to avoid using ASID?

BTW, I have seen ASID management in seL4 (ASID control and ASID pool), so maybe I misunderstood something?

Dong Du,
Shanghai Jiao Tong University