Subject: Re: [PATCH RFC 11/14] arm64: Move the ASID allocator code in a separate file

From: Catalin Marinas <[email-masked]>
Date: Mon, 24 Jun 2019 16:38:20 +0100

On Mon, Jun 24, 2019 at 12:35:35AM +0800, Guo Ren wrote:
> On Fri, Jun 21, 2019 at 10:16 PM Catalin Marinas
> <[email-masked]> 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

_______________________________________________
linux-arm-kernel mailing list
[email-masked]
http://lists.infradead.org/mailman/listinfo/linux-arm-kernel