linux-kernel - Re: [PATCH] tools/memory-model: Remove lock-final checking in lock.cat

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Date:   Wed, 26 Feb 2020 09:58:12 -0500 (EST)
From:   Alan Stern <stern@...land.harvard.edu>
To:     Boqun Feng <boqun.feng@...il.com>
cc:     linux-kernel@...r.kernel.org, <rcu@...r.kernel.org>,
        Andrea Parri <parri.andrea@...il.com>,
        Will Deacon <will@...nel.org>,
        Peter Zijlstra <peterz@...radead.org>,
        Nicholas Piggin <npiggin@...il.com>,
        David Howells <dhowells@...hat.com>,
        Jade Alglave <j.alglave@....ac.uk>,
        Luc Maranget <luc.maranget@...ia.fr>,
        "Paul E. McKenney" <paulmck@...nel.org>,
        Akira Yokosawa <akiyks@...il.com>,
        Daniel Lustig <dlustig@...dia.com>,
        <linux-arch@...r.kernel.org>
Subject: Re: [PATCH] tools/memory-model: Remove lock-final checking in lock.cat

On Wed, 26 Feb 2020, Boqun Feng wrote:

> In commit 30b795df11a1 ("tools/memory-model: Improve mixed-access
> checking in lock.cat"), we have added the checking to disallow any
> normal memory access to lock variables, and this checking is stronger
> than lock-final. So remove the lock-final checking as it's unnecessary
> now.

I don't understand this description.  Why do you say that the
normal-access checking is stronger than the lock-final check?

> Signed-off-by: Boqun Feng <boqun.feng@...il.com>
> ---
>  tools/memory-model/lock.cat | 3 ---
>  1 file changed, 3 deletions(-)
> 
> diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
> index 6b52f365d73a..827a3646607c 100644
> --- a/tools/memory-model/lock.cat
> +++ b/tools/memory-model/lock.cat
> @@ -54,9 +54,6 @@ flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
>   *)
>  empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
>  
> -(* The final value of a spinlock should not be tested *)
> -flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
> -
>  (*
>   * Put lock operations in their appropriate classes, but leave UL out of W
>   * until after the co relation has been generated.

With this check removed, what will prevent people from writing litmus 
tests like this?

C test

{
	spinlock_t s;
}

...

exists (s=0)

Alan