Re: kernel/rcu/srcutree.c:1644 srcu_advance_state() warn: inconsistent returns '&ssp->srcu_sup->srcu_gp_mutex'.

[Dan Carpenter]

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...

regards,
dan carpenter

diff --git a/kernel/rcu/srcutree.c b/kernel/rcu/srcutree.c
index 20d7a238d675..58e13d3c5a6a 100644
--- a/kernel/rcu/srcutree.c
+++ b/kernel/rcu/srcutree.c
@@ -1669,6 +1669,8 @@ static void srcu_advance_state(struct srcu_struct *ssp)
 		}
 		ssp->srcu_sup->srcu_n_exp_nodelay = 0;
 		srcu_gp_end(ssp);  /* Releases ->srcu_gp_mutex. */
+	} else {
+		unreachable();
 	}
 }