Re: [PATCH] tools/memory-model: Explain syntactic and semantic dependencies

From: Alan Stern
Date: Tue Feb 01 2022 - 13:53:19 EST


On Tue, Feb 01, 2022 at 10:02:39AM -0800, Paul E. McKenney wrote:
> On Thu, Jan 27, 2022 at 04:11:48PM -0500, Alan Stern wrote:
> > Paul Heidekrüger pointed out that the Linux Kernel Memory Model
> > documentation doesn't mention the distinction between syntactic and
> > semantic dependencies. This is an important difference, because the
> > compiler can easily break dependencies that are only syntactic, not
> > semantic.
> >
> > This patch adds a few paragraphs to the LKMM documentation explaining
> > these issues and illustrating how they can matter.
> >
> > Suggested-by: Paul Heidekrüger <paul.heidekrueger@xxxxxxxxx>
> > Signed-off-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> >
> > ---
> >
> >
> > [as1970]
> >
> >
> > tools/memory-model/Documentation/explanation.txt | 47 +++++++++++++++++++++++
> > 1 file changed, 47 insertions(+)
> >
> > Index: usb-devel/tools/memory-model/Documentation/explanation.txt
> > ===================================================================
> > --- usb-devel.orig/tools/memory-model/Documentation/explanation.txt
> > +++ usb-devel/tools/memory-model/Documentation/explanation.txt
> > @@ -485,6 +485,53 @@ have R ->po X. It wouldn't make sense f
> > somehow on a value that doesn't get loaded from shared memory until
> > later in the code!
> >
> > +Here's a trick question: When is a dependency not a dependency? Answer:
> > +When it is purely syntactic rather than semantic. We say a dependency
> > +between two accesses is purely syntactic if the second access doesn't
> > +actually depend on the result of the first. Here is a trivial example:
> > +
> > + r1 = READ_ONCE(x);
> > + WRITE_ONCE(y, r1 * 0);
> > +
> > +There appears to be a data dependency from the load of x to the store of
> > +y, since the value to be stored is computed from the value that was
> > +loaded. But in fact, the value stored does not really depend on
> > +anything since it will always be 0. Thus the data dependency is only
> > +syntactic (it appears to exist in the code) but not semantic (the second
> > +access will always be the same, regardless of the value of the first
> > +access). Given code like this, a compiler could simply eliminate the
> > +load from x, which would certainly destroy any dependency.
>
> Are you OK with that last sentence reading as follows?
>
> Given code like this, a compiler could simply discard the value
> return by the load from x, which would certainly destroy any

s/return/returned/

> dependency.
>
> My concern with the original is that it might mislead people into thinking
> that compilers can omit volatile loads.

Yes, good point. Should we also tack on something like this?

(The compiler is not permitted to eliminate entirely the load
generated for a READ_ONCE() -- that's one of the nice properties
of READ_ONCE() -- but it is allowed to ignore the load's value.)

> > +
> > +(It's natural to object that no one in their right mind would write code
> > +like the above. However, macro expansions can easily give rise to this
> > +sort of thing, in ways that generally are not apparent to the
> > +programmer.)
> > +
> > +Another mechanism that can give rise to purely syntactic dependencies is
> > +related to the notion of "undefined behavior". Certain program behaviors
> > +are called "undefined" in the C language specification, which means that
> > +when they occur there are no guarantees at all about the outcome.
> > +Consider the following example:
> > +
> > + int a[1];
> > + int i;
> > +
> > + r1 = READ_ONCE(i);
> > + r2 = READ_ONCE(a[r1]);
> > +
> > +Access beyond the end or before the beginning of an array is one kind of
> > +undefined behavior. Therefore the compiler doesn't have to worry about
> > +what will happen if r1 is nonzero, and it can assume that r1 will always
> > +be zero without actually loading anything from i.
>
> And similarly here:
>
> ... and it can assume that r1 will always be zero regardless of
> the value actually loaded from i.

Right.

> > + (If the assumption
> > +turns out to be wrong, the resulting behavior will be undefined anyway
> > +so the compiler doesn't care!) Thus the load from i can be eliminated,
> > +breaking the address dependency.

This also should be changed:

Thus the value from the load can be discarded, breaking the
address dependency.

> > +
> > +The LKMM is unaware that purely syntactic dependencies are different
> > +from semantic dependencies and therefore mistakenly predicts that the
> > +accesses in the two examples above will be ordered. This is another
> > +example of how the compiler can undermine the memory model. Be warned.
> > +
> >
> > THE READS-FROM RELATION: rf, rfi, and rfe
> > -----------------------------------------
>
> Looks great otherwise, and thank you all for your work on this!
>
> Alan, would you like me to pull this in making those two changes and
> applying Akira's Reviewed-by, or would you prefer to send another version?

I'll send a new version.

> For that matter, am I off base in my suggested changes.

Not at all. Thanks.

Alan