On Fri, Sep 10, 2021 at 09:06:31AM +0000, Shameerali Kolothum Thodi wrote: > > [2] https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git/commit/ > > I am going through the ASID TLA+ model and in the above commit, it appears that the > different ASID check(=> ActiveAsid(c1) # ActiveAsid(c2)) for the Invariant > UniqueASIDActiveTask is now removed. > > Just wondering why that is not relevant anymore? It's still relevant. I probably deleted it by mistake, I'll add it back now. Thanks for carefully looking at this commit. -- Catalin
