Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) client-ip=2620:137:e000::1:20;
Date:   Tue, 16 May 2023 12:46:53 -0700
From:   "Paul E. McKenney" <paulmck@kernel.org>
To:     Dan Carpenter <dan.carpenter@linaro.org>
Cc:     oe-kbuild@lists.linux.dev, lkp@intel.com,
        oe-kbuild-all@lists.linux.dev, linux-kernel@vger.kernel.org
Subject: Re: kernel/rcu/srcutree.c:1644 srcu_advance_state() warn:
 inconsistent returns '&ssp->srcu_sup->srcu_gp_mutex'.
Message-ID: <4de09952-297c-45c1-9cd9-b847293f5887@paulmck-laptop>
Reply-To: paulmck@kernel.org
References: <c0937326-1cf1-429a-9883-30d9d79b01d0@kili.mountain>
 <c33b0348-7f86-47ce-913c-f1ebc6431f93@paulmck-laptop>
 <30f2e760-e2f3-4941-be9b-b9c5624fd861@kili.mountain>
 <4bdbbcd3-6620-4320-ada5-02b71a54106c@paulmck-laptop>
 <782b3fa6-576d-4c26-888e-5dc151feaaa8@kili.mountain>
 <2ef061eb-e82d-4c16-a333-e499095a7162@paulmck-laptop>
 <0e191d4f-43ad-476a-92e0-d038715b25ca@kili.mountain>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <0e191d4f-43ad-476a-92e0-d038715b25ca@kili.mountain>
Precedence: bulk

On Tue, May 16, 2023 at 03:21:55PM +0300, Dan Carpenter wrote:
> On Tue, May 16, 2023 at 05:17:57AM -0700, Paul E. McKenney wrote:
> > On Tue, May 09, 2023 at 06:13:02PM +0300, Dan Carpenter wrote:
> > > On Tue, May 09, 2023 at 07:08:05AM -0700, Paul E. McKenney wrote:
> > > > On Tue, May 09, 2023 at 08:40:33AM +0300, Dan Carpenter wrote:
> > > > > On Sat, May 06, 2023 at 11:45:35AM -0700, Paul E. McKenney wrote:
> > > > > > On Sat, May 06, 2023 at 10:22:04AM +0300, Dan Carpenter wrote:
> > > > > > > aacb5d91ab1bfb Paul E. McKenney 2018-10-28  1632  	if (rcu_seq_state(READ_ONCE(ssp->srcu_gp_seq)) == SRCU_STATE_SCAN2) {
> > > > > > > 
> > > > > > > We don't mutex_unlock(&ssp->srcu_sup->srcu_gp_mutex) if this if
> > > > > > > statement is false.
> > > > > > 
> > > > > > Hmmm...
> > > > > > 
> > > > > > I could make the above line read something like the following:
> > > > > > 
> > > > > > 	if (!WARN_ON_ONCE(rcu_seq_state(READ_ONCE(ssp->srcu_sup->srcu_gp_seq)) != SRCU_STATE_SCAN2)) {
> > > > > 
> > > > > Smatch ignores WARN_ON().  WARNings are triggered all the time, so it's
> > > > > not like a BUG() which stops the code flow.
> > > > > 
> > > > > > 
> > > > > > The theory is that there are only three legal values for ->srcu_gp_seq.
> > > > > > Because we hold ->srcu_gp_mutex, no one else can change it.   The first
> > > > > > "if" statement either returns or sets that state to SRCU_STATE_SCAN1.
> > > > > > The second "if" statement also either returns or sets that state to
> > > > > > SRCU_STATE_SCAN2.  So that statement should not be false.
> > > > > 
> > > > > Smatch can't figure out that the statement is true.  The issue there is
> > > > > that ssp->srcu_sup->srcu_gp_seq stores a value in the low bits and a
> > > > > different value in the high bits.  This seems like something that might
> > > > > be worth handling correctly at some point, but that point is in the
> > > > > distant future...
> > > > > 
> > > > > Just ignore this one.
> > > > 
> > > > Fair enough!  Yeah, I could imagine that this would be non-trivial.
> > > > 
> > > > Is there a not-reached annotation that Smatch pays attention to?
> > > 
> > > Hm...  Yeah.  If you wanted you could do this.  I'm not sure it improves
> > > the readability.  Also for some reason my private Smatch build doesn't
> > > print a warning...  I need to investigate why that is...
> > 
> > There does seem to be a fair number of instances of unreachable() in
> > the kernel, so why not?
> > 
> > May I add your Signed-off-by?
> 
> Sure.  I probably does make it more readable to some people as well.
> (It's a very narrow band of people who it helps).
> 
> Signed-off-by: Dan Carpenter <dan.carpenter@linaro.org>

Except that this got me the following:

vmlinux.o: warning: objtool: process_srcu() falls through to next function same_state_synchronize_rcu()

Adding explicit return statements did not help.

Thoughts?

							Thanx, Paul