[<prev] [next>] [<thread-prev] [day] [month] [year] [list]
Message-ID: <6400b843-33b7-44fe-97dc-7a8c737ac6cc@paulmck-laptop>
Date: Fri, 11 Jul 2025 11:41:12 -0700
From: "Paul E. McKenney" <paulmck@...nel.org>
To: Joel Fernandes <joelagnelf@...dia.com>
Cc: linux-kernel@...r.kernel.org, Frederic Weisbecker <frederic@...nel.org>,
Neeraj Upadhyay <neeraj.upadhyay@...nel.org>,
Josh Triplett <josh@...htriplett.org>,
Boqun Feng <boqun.feng@...il.com>,
Uladzislau Rezki <urezki@...il.com>,
Steven Rostedt <rostedt@...dmis.org>,
Mathieu Desnoyers <mathieu.desnoyers@...icios.com>,
Lai Jiangshan <jiangshanlai@...il.com>,
Zqiang <qiang.zhang@...ux.dev>, rcu@...r.kernel.org
Subject: Re: [PATCH -rcu -next 4/7] rcu: Remove redundant check for irq state
during unlock
On Fri, Jul 11, 2025 at 02:19:47PM -0400, Joel Fernandes wrote:
>
>
> On 7/11/2025 1:18 PM, Paul E. McKenney wrote:
> > On Fri, Jul 11, 2025 at 12:30:08PM -0400, Joel Fernandes wrote:
> >>
> >>
> >> On 7/10/2025 8:00 PM, Paul E. McKenney wrote:
> >>> On Tue, Jul 08, 2025 at 10:22:21AM -0400, Joel Fernandes wrote:
> >>>> The check for irqs_were_disabled is redundant in
> >>>> rcu_unlock_needs_exp_handling() as the caller already checks for this.
> >>>> This includes the boost case as well. Just remove the redundant check.
> >>>
> >>> But in the very last "if" statement in the context of the last hunk of
> >>> this patch, isn't it instead checking for !irqs_were_disabled?
> >>>
> >>> Or is there something that I am missing that makes this work out OK?
> >>
> >> You are right, after going over all the cases I introduced a behavioral change.
> >>
> >> Say, irqs_were_disabled was false. And say we are RCU-boosted. needs_exp might
> >> return true now, but previously it was returning false. Further say, we are not
> >> in hardirq.
> >>
> >> New code will raise softirq, old code would go to the ELSE and just set:
> >> set_tsk_need_resched(current);
> >> set_preempt_need_resched();
> >>
> >> But preempt_bh_were_disabled that's why we're here.
> >>
> >> So we need to only set resched and not raise softirq, because the preempt enable
> >> would reschedule.
> >>
> >> Sorry I missed this, but unless this behavior is correct or needs further work,
> >> lets drop this patch. Thanks and kudos on the catch!
> >
> > Not a problem!
> >
> > You can use cbmc to check these sorts of transformations, as described
> > here: https://paulmck.livejournal.com/38997.html
>
> Much appreciated! Does the tool automatically create stubs for dependent
> structures or is that upto the CBMC user? I see in your example in the blog you
> did create an rcu_node :). I wonder if for large number of dependencies on the
> code base, how it does in terms of overhead for the user.
You do need to create the stubs. But you also have the option of
simplifying the code, for example, by removing structure fields that
you are not using and providing static instances of the needed structures.
> But perhaps for simpler examples (such as perhaps the above), manually mocking
> data structures and dependent code is reasonable?
That is what I do. ;-)
> We'd have to stub irq_work and raise_softirq and functions too and also the
> CONFIG option values.
Agreed. But in this case, we only need to know whether or not they
were called, so a very simple stub suffices.
You can also speed things up by replacing the Kconfig options with
variables, thus allowing full exploration in one run. And dispensing
with the dazzling implementation of IS_ENABLED(). ;-)
Thanx, Paul
Powered by blists - more mailing lists