Hi Dong,

Per my understanding, "isb" and "dsb" do not flush TLB. "isb" has t??he 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.?

ASID is used to reduce TLB flushes.

Regards,

Yanyan?

________________________________ 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