Date:   Wed, 25 Jan 2023 09:27:50 -0800
From:   "Paul E. McKenney" <paulmck@kernel.org>
To:     Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Cc:     Alan Stern <stern@rowland.harvard.edu>, parri.andrea@gmail.com,
        will@kernel.org, peterz@infradead.org, boqun.feng@gmail.com,
        npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk,
        luc.maranget@inria.fr, akiyks@gmail.com, dlustig@nvidia.com,
        joel@joelfernandes.org, urezki@gmail.com, quic_neeraju@quicinc.com,
        frederic@kernel.org, linux-kernel@vger.kernel.org
Subject: Re: [PATCH] tools/memory-model Flag suspicious use of srcu cookies
Message-ID: <20230125172750.GA1522225@paulmck-ThinkPad-P17-Gen-1>
Reply-To: paulmck@kernel.org
References: <20230124143951.23372-1-jonas.oberhauser@huaweicloud.com>
 <Y9ATHMm/iVG8goln@rowland.harvard.edu>
 <20230124191535.GT2948950@paulmck-ThinkPad-P17-Gen-1>
 <87b8e8ba-a53d-c3e5-1478-9e6cc2b78fee@huaweicloud.com>
 <20230124221915.GW2948950@paulmck-ThinkPad-P17-Gen-1>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <20230124221915.GW2948950@paulmck-ThinkPad-P17-Gen-1>
Precedence: bulk

On Tue, Jan 24, 2023 at 02:19:15PM -0800, Paul E. McKenney wrote:
> On Tue, Jan 24, 2023 at 08:36:53PM +0100, Jonas Oberhauser wrote:
> > 
> > 
> > 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@huaweicloud.com>
> > > > > ---
> > > > Acked-by: Alan Stern <stern@rowland.harvard.edu>
> > > 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.
> 
> You got it right.
> 
> > 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 : )
> 
> No I didn't!  I missed *two*!  ;-)
> 
> Though that comment could be Srcu-unlock, I suppose.  But making it
> srcu_read_unlock() seems more straightforward.  Update below!

And I also added this to the lkmm-srcu.2023.01.20a branch just for
experimental purposes.

							Thanx, Paul