lkml.org 
[lkml]   [2019]   [Jun]   [24]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    /
    Date
    From
    SubjectRe: [PATCH RFC 11/14] arm64: Move the ASID allocator code in a separate file
    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.marinas@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

    \
     
     \ /
      Last update: 2019-06-24 17:38    [W:3.089 / U:1.444 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site