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