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?