From mboxrd@z Thu Jan 1 00:00:00 1970 From: Andrea Parri Subject: Re: [PATCH RFC LKMM 7/7] tools/memory-model: Dynamically check SRCU lock-to-unlock matching Date: Thu, 10 Jan 2019 10:41:31 +0100 Message-ID: <20190110094131.GA11647@andrea> References: <20190109210706.GA27268@linux.ibm.com> <20190109210748.29074-7-paulmck@linux.ibm.com> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Return-path: Content-Disposition: inline In-Reply-To: <20190109210748.29074-7-paulmck@linux.ibm.com> Sender: linux-kernel-owner@vger.kernel.org To: "Paul E. McKenney" Cc: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, mingo@kernel.org, stern@rowland.harvard.edu, parri.andrea@gmail.com, will.deacon@arm.com, peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr, willy@infradead.org List-Id: linux-arch.vger.kernel.org On Wed, Jan 09, 2019 at 01:07:48PM -0800, Paul E. McKenney wrote: > From: Luc Maranget > > This commit checks that the return value of srcu_read_lock() is passed > to the matching srcu_read_unlock(), where "matching" is determined by > nesting. This check operates as follows: > > 1. srcu_read_lock() creates an integer token, which is stored into > the generated events. > 2. srcu_read_unlock() records its second (token) argument into the > generated event. > 3. A new herd primitive 'different-values' filters out pairs of events > with identical values from the relation passed as its argument. > 4. The bell file applies the above primitive to the (srcu) > read-side-critical-section relation 'srcu-rscs' and flags non-empty > results. > > BEWARE: Works only with herd version 7.51+6 and onwards. > > Signed-off-by: Luc Maranget > Signed-off-by: Paul E. McKenney > [ paulmck: Apply Andrea Parri's off-list feedback. ] > --- > tools/memory-model/linux-kernel.bell | 3 +++ > tools/memory-model/linux-kernel.cat | 2 ++ > tools/memory-model/linux-kernel.def | 2 +- > 3 files changed, 6 insertions(+), 1 deletion(-) > > diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell > index 9c42cd9ddcb4..def9131d3d8e 100644 > --- a/tools/memory-model/linux-kernel.bell > +++ b/tools/memory-model/linux-kernel.bell > @@ -73,3 +73,6 @@ flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking > > (* Check for use of synchronize_srcu() inside an RCU critical section *) > flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep > + > +(* Validate SRCU dynamic match *) > +flag ~empty different-values(srcu-rscs) as srcu-bad-nesting > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat > index 8dcb37835b61..95bf45f1215f 100644 > --- a/tools/memory-model/linux-kernel.cat > +++ b/tools/memory-model/linux-kernel.cat > @@ -1,5 +1,7 @@ > // SPDX-License-Identifier: GPL-2.0+ > (* > + * Requires herd version 7.51+6 or higher. I'm not all that exited about spreading version requirements in the source: we report this requirement in our README, and apparently we already struggle to keep this information up-to-date. So what about squashing something like the below (assume that 7.52 will be released by the time this patch hit mainline; if this won't be the case, we may consider using the development version 7.51+6)? notice that this also removes an (obsolete, at this point) comment from lock.cat. Andrea diff --git a/tools/memory-model/README b/tools/memory-model/README index 9d7d4f23503fd..b362a41358fa1 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -20,8 +20,8 @@ that litmus test to be exercised within the Linux kernel. REQUIREMENTS ============ -Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded -separately: +Version 7.52 or higher of the "herd7" and "klitmus7" tools must be +downloaded separately: https://github.com/herd/herdtools7 diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index 95bf45f1215fc..8dcb37835b613 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -1,7 +1,5 @@ // SPDX-License-Identifier: GPL-2.0+ (* - * Requires herd version 7.51+6 or higher. - * * Copyright (C) 2015 Jade Alglave , * Copyright (C) 2016 Luc Maranget for Inria * Copyright (C) 2017 Alan Stern , diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat index 305ded17e7411..a059d1a6d8a29 100644 --- a/tools/memory-model/lock.cat +++ b/tools/memory-model/lock.cat @@ -6,9 +6,6 @@ (* * Generate coherence orders and handle lock operations - * - * Warning: spin_is_locked() crashes herd7 versions strictly before 7.48. - * spin_is_locked() is functional from herd7 version 7.49. *) include "cross.cat" > + * > * Copyright (C) 2015 Jade Alglave , > * Copyright (C) 2016 Luc Maranget for Inria > * Copyright (C) 2017 Alan Stern , > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def > index 1d6a120cde14..0c3f0ef486f4 100644 > --- a/tools/memory-model/linux-kernel.def > +++ b/tools/memory-model/linux-kernel.def > @@ -49,7 +49,7 @@ synchronize_rcu_expedited() { __fence{sync-rcu}; } > > // SRCU > srcu_read_lock(X) __srcu{srcu-lock}(X) > -srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X); } > +srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); } > synchronize_srcu(X) { __srcu{sync-srcu}(X); } > > // Atomic > -- > 2.17.1 > From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-ed1-f68.google.com ([209.85.208.68]:44673 "EHLO mail-ed1-f68.google.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1727961AbfAJJlr (ORCPT ); Thu, 10 Jan 2019 04:41:47 -0500 Received: by mail-ed1-f68.google.com with SMTP id y56so9630917edd.11 for ; Thu, 10 Jan 2019 01:41:45 -0800 (PST) Date: Thu, 10 Jan 2019 10:41:31 +0100 From: Andrea Parri Subject: Re: [PATCH RFC LKMM 7/7] tools/memory-model: Dynamically check SRCU lock-to-unlock matching Message-ID: <20190110094131.GA11647@andrea> References: <20190109210706.GA27268@linux.ibm.com> <20190109210748.29074-7-paulmck@linux.ibm.com> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20190109210748.29074-7-paulmck@linux.ibm.com> Sender: linux-arch-owner@vger.kernel.org List-ID: To: "Paul E. McKenney" Cc: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, mingo@kernel.org, stern@rowland.harvard.edu, parri.andrea@gmail.com, will.deacon@arm.com, peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr, willy@infradead.org Message-ID: <20190110094131.SqZfycc-GypJYWQ5-CnKcQVOsxofrE5uOe0iLQTXg1Y@z> On Wed, Jan 09, 2019 at 01:07:48PM -0800, Paul E. McKenney wrote: > From: Luc Maranget > > This commit checks that the return value of srcu_read_lock() is passed > to the matching srcu_read_unlock(), where "matching" is determined by > nesting. This check operates as follows: > > 1. srcu_read_lock() creates an integer token, which is stored into > the generated events. > 2. srcu_read_unlock() records its second (token) argument into the > generated event. > 3. A new herd primitive 'different-values' filters out pairs of events > with identical values from the relation passed as its argument. > 4. The bell file applies the above primitive to the (srcu) > read-side-critical-section relation 'srcu-rscs' and flags non-empty > results. > > BEWARE: Works only with herd version 7.51+6 and onwards. > > Signed-off-by: Luc Maranget > Signed-off-by: Paul E. McKenney > [ paulmck: Apply Andrea Parri's off-list feedback. ] > --- > tools/memory-model/linux-kernel.bell | 3 +++ > tools/memory-model/linux-kernel.cat | 2 ++ > tools/memory-model/linux-kernel.def | 2 +- > 3 files changed, 6 insertions(+), 1 deletion(-) > > diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell > index 9c42cd9ddcb4..def9131d3d8e 100644 > --- a/tools/memory-model/linux-kernel.bell > +++ b/tools/memory-model/linux-kernel.bell > @@ -73,3 +73,6 @@ flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking > > (* Check for use of synchronize_srcu() inside an RCU critical section *) > flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep > + > +(* Validate SRCU dynamic match *) > +flag ~empty different-values(srcu-rscs) as srcu-bad-nesting > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat > index 8dcb37835b61..95bf45f1215f 100644 > --- a/tools/memory-model/linux-kernel.cat > +++ b/tools/memory-model/linux-kernel.cat > @@ -1,5 +1,7 @@ > // SPDX-License-Identifier: GPL-2.0+ > (* > + * Requires herd version 7.51+6 or higher. I'm not all that exited about spreading version requirements in the source: we report this requirement in our README, and apparently we already struggle to keep this information up-to-date. So what about squashing something like the below (assume that 7.52 will be released by the time this patch hit mainline; if this won't be the case, we may consider using the development version 7.51+6)? notice that this also removes an (obsolete, at this point) comment from lock.cat. Andrea diff --git a/tools/memory-model/README b/tools/memory-model/README index 9d7d4f23503fd..b362a41358fa1 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -20,8 +20,8 @@ that litmus test to be exercised within the Linux kernel. REQUIREMENTS ============ -Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded -separately: +Version 7.52 or higher of the "herd7" and "klitmus7" tools must be +downloaded separately: https://github.com/herd/herdtools7 diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index 95bf45f1215fc..8dcb37835b613 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -1,7 +1,5 @@ // SPDX-License-Identifier: GPL-2.0+ (* - * Requires herd version 7.51+6 or higher. - * * Copyright (C) 2015 Jade Alglave , * Copyright (C) 2016 Luc Maranget for Inria * Copyright (C) 2017 Alan Stern , diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat index 305ded17e7411..a059d1a6d8a29 100644 --- a/tools/memory-model/lock.cat +++ b/tools/memory-model/lock.cat @@ -6,9 +6,6 @@ (* * Generate coherence orders and handle lock operations - * - * Warning: spin_is_locked() crashes herd7 versions strictly before 7.48. - * spin_is_locked() is functional from herd7 version 7.49. *) include "cross.cat" > + * > * Copyright (C) 2015 Jade Alglave , > * Copyright (C) 2016 Luc Maranget for Inria > * Copyright (C) 2017 Alan Stern , > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def > index 1d6a120cde14..0c3f0ef486f4 100644 > --- a/tools/memory-model/linux-kernel.def > +++ b/tools/memory-model/linux-kernel.def > @@ -49,7 +49,7 @@ synchronize_rcu_expedited() { __fence{sync-rcu}; } > > // SRCU > srcu_read_lock(X) __srcu{srcu-lock}(X) > -srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X); } > +srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); } > synchronize_srcu(X) { __srcu{sync-srcu}(X); } > > // Atomic > -- > 2.17.1 >