Re: [PATCH] tools/memory-model Flag suspicious use of srcu cookies

[Jonas Oberhauser]

On 1/24/2023 8:15 PM, Paul E. McKenney wrote:
> On Tue, Jan 24, 2023 at 12:19:24PM -0500, Alan Stern wrote:
> > On Tue, Jan 24, 2023 at 03:39:51PM +0100, Jonas Oberhauser wrote:
> > > The herd model of LKMM deviates from actual implementations in the
> > > range of cookies that might be returned by srcu_lock() and similar
> > > functions.  As a consequence, code that relies on srcu_lock()
> > > returning specific values might pass on the herd model but fail in
> > > the real world.
> > >
> > > This patch flags any code that looks at the value of a cookie
> > > without passing it on to an srcu_unlock().  This indicates that the
> > > cookie value might be being used in ways that can lead herd to
> > > produce incorrect results, as in the following (contrived) case:
> > >
> > > P0(struct srcu_struct *ss)
> > > {
> > > 	int r = srcu_read_lock(ss);
> > > 	if (r==0)
> > > 		srcu_read_unlock(ss, r);
> > > }
> > >
> > > Without this patch, the code passes herd7 without any warnings.
> > >
> > > With this patch, this code is flagged with illegal-srcu-cookie-ctrl,
> > > indicating that a cookie is used to compute a control condition.
> > > Such scenarios potentially lead to other branches of the code that
> > > are possible in real usage not being evaluated by herd7.  In this
> > > example, this affects the branch where r!=0, which would lead to
> > > an unmatched read side critical section and thus to hangs of
> > > synchronize_srcu() calls.
> > >
> > > Besides use of cookies in control conditions, the patch also flags
> > > use in address computation and any time a cookie is inspected but
> > > not later passed to srcu_read_unlock().
> > >
> > > Signed-off-by: Jonas Oberhauser <jonas.oberhauser@xxxxxxxxxxxxxxx>
> > > ---
> > Acked-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> Thank you both!
>
> I wordsmithed the commit log as follows, but then realized that this
> depends on Alan's earlier patch.

Yeah, I don't know if I did this correctly. I based it on the 
lkmm-srcu.2023.01.20a branch.
Let me know if I should have done this differently.

Looking through your changes to learn for future submissions:

> [...]
>
> This patch flags any code that looks at the value of a cookie
> without passing it on to an srcu_unlock().

You missed this one : )

Have fun, jonas