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.
But perhaps for simpler examples (such as perhaps the above), manually mocking
data structures and dependent code is reasonable?
We'd have to stub irq_work and raise_softirq and functions too and also the
CONFIG option values.
Thanks!
- Joel
