[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <20200901014504.GB571008@rowland.harvard.edu>
Date: Mon, 31 Aug 2020 21:45:04 -0400
From: Alan Stern <stern@...land.harvard.edu>
To: "Paul E. McKenney" <paulmck@...nel.org>
Cc: linux-kernel@...r.kernel.org, linux-arch@...r.kernel.org,
kernel-team@...com, mingo@...nel.org, parri.andrea@...il.com,
will@...nel.org, peterz@...radead.org, boqun.feng@...il.com,
npiggin@...il.com, dhowells@...hat.com, j.alglave@....ac.uk,
luc.maranget@...ia.fr, akiyks@...il.com
Subject: Re: [PATCH kcsan 9/9] tools/memory-model: Document locking corner
cases
On Mon, Aug 31, 2020 at 02:47:38PM -0700, Paul E. McKenney wrote:
> On Mon, Aug 31, 2020 at 04:17:01PM -0400, Alan Stern wrote:
> > Is this discussion perhaps overkill?
> >
> > Let's put it this way: Suppose we have the following code:
> >
> > P0(int *x, int *lck)
> > {
> > spin_lock(lck);
> > WRITE_ONCE(*x, 1);
> > do_something();
> > spin_unlock(lck);
> > }
> >
> > P1(int *x, int *lck)
> > {
> > while (READ_ONCE(*x) == 0)
> > ;
> > spin_lock(lck);
> > do_something_else();
> > spin_unlock(lck);
> > }
> >
> > It's obvious that this test won't deadlock. But if P1 is changed to:
> >
> > P1(int *x, int *lck)
> > {
> > spin_lock(lck);
> > while (READ_ONCE(*x) == 0)
> > ;
> > do_something_else();
> > spin_unlock(lck);
> > }
> >
> > then it's equally obvious that the test can deadlock. No need for
> > fancy memory models or litmus tests or anything else.
>
> For people like you and me, who have been thinking about memory ordering
> for longer than either of us care to admit, this level of exposition is
> most definitely -way- overkill!!!
>
> But I have had people be very happy and grateful that I explained this to
> them at this level of detail. Yes, I started parallel programming before
> some of them were born, but they are definitely within our target audience
> for this particular document. And it is not just Linux kernel hackers
> who need this level of detail. A roughly similar transactional-memory
> scenario proved to be so non-obvious to any number of noted researchers
> that Blundell, Lewis, and Martin needed to feature it in this paper:
> https://ieeexplore.ieee.org/abstract/document/4069174
> (Alternative source: https://repository.upenn.edu/cgi/viewcontent.cgi?article=1344&context=cis_papers)
>
> Please note that I am -not- advocating making (say) explanation.txt or
> recipes.txt more newbie-accessible than they already are. After all,
> the point of the README file in that same directory is to direct people
> to the documentation files that are the best fit for them, and both
> explanation.txt and recipes.txt contain advanced material, and thus
> require similarly advanced prerequisites.
>
> Seem reasonable, or am I missing your point?
The question is, what are you trying to accomplish in this section? Are
you trying to demonstrate that it isn't safe to allow arbitrary code to
leak into a critical section? If so then you don't need to present an
LKMM litmus test to make the point; the example I gave here will do
quite as well. Perhaps even better, since it doesn't drag in all sorts
of extraneous concepts like limitations of litmus tests or how to
emulate a spin loop.
On the other hand, if your goal is to show how to construct a litmus
test that will model a particular C language test case (such as the one
I gave), then the text does a reasonable job -- although I do think it
could be clarified somewhat. For instance, it wouldn't hurt to include
the real C code before giving the corresponding litmus test, so that the
reader will have a clear idea of what you're trying to model.
Just what you want to achieve here is not clear from the context.
Besides, the example is in any case a straw man. The text starts out
saying "It is tempting to allow memory-reference instructions to be
pulled into a critical section", but then the example pulls an entire
spin loop inside -- not just the memory references but also the
conditional branch instruction at the bottom of the loop! I can't
imagine anyone would think it was safe to allow branches to leak into a
critical section, particularly when doing so would break a control
dependency (as it does here).
Alan
Powered by blists - more mailing lists