Messages in this thread | | | Date | Wed, 25 Jan 2023 09:27:50 -0800 | From | "Paul E. McKenney" <> | Subject | Re: [PATCH] tools/memory-model Flag suspicious use of srcu cookies |
| |
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
| |