On Mon, Jun 24, 2019 at 12:35:35AM +0800, Guo Ren wrote: > On Fri, Jun 21, 2019 at 10:16 PM Catalin Marinas > <catalin.mari...@arm.com> wrote: > > BTW, if you find the algorithm fairly straightforward ;), see this > > bug-fix which took a formal model to identify: a8ffaaa060b8 ("arm64: > > asid: Do not replace active_asids if already 0"). [...] > Btw, Is this detected by arm's aisd allocator TLA+ model ? Or a real > bug report ?
This specific bug was found by the TLA+ model checker (at the time we were actually tracking down another bug with multi-threaded CPU sharing the TLB, bug also confirmed by the formal model). -- Catalin