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

[Paul Heidekrüger]

On Tue, Jan 25, 2022 at 04:00:11PM -0500, Alan Stern wrote:
> On Tue, Jan 25, 2022 at 05:28:19PM +0000, Paul Heidekrüger wrote:
> > Dependencies which are purely syntactic, i.e. not semantic, might imply
> > ordering at first glance. However, since they do not affect defined
> > behavior, compilers are within their rights to remove such dependencies
> > when optimizing code.
> > 
> > Since syntactic dependencies are not related to any kind of dependency
> > in particular, explicitly distinguish syntactic and semantic
> > dependencies as part of the 'A WARNING' section in explanation.txt,
> > which gives examples of how compilers might affect the LKMM's dependency
> > orderings in general.
> 
> The "A WARNING" section is a bad place to put this material, because it 
> comes before dependencies have been introduced.  It would be better to 
> put this at the end of the "DEPENDENCY RELATIONS: data, addr, and ctrl" 
> section.
> 
> > Link: https://lore.kernel.org/all/20211102190138.GA1497378@xxxxxxxxxxxxxxxxxxx/
> > Signed-off-by: Paul Heidekrüger <paul.heidekrueger@xxxxxxxxx>
> > Cc: Marco Elver <elver@xxxxxxxxxx>
> > Cc: Charalampos Mainas <charalampos.mainas@xxxxxxxxx>
> > Cc: Pramod Bhatotia <pramod.bhatotia@xxxxxxxxx>
> > ---
> >  .../Documentation/explanation.txt             | 25 +++++++++++++++++++
> >  1 file changed, 25 insertions(+)
> > 
> > diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> > index 5d72f3112e56..6d679e5ebdf9 100644
> > --- a/tools/memory-model/Documentation/explanation.txt
> > +++ b/tools/memory-model/Documentation/explanation.txt
> > @@ -411,6 +411,31 @@ Given this version of the code, the LKMM would predict that the load
> >  from x could be executed after the store to y.  Thus, the memory
> >  model's original prediction could be invalidated by the compiler.
> >  
> > +Caution is also advised when dependencies are purely syntactic, i.e.
> > +not semantic.  A dependency between two marked accesses is purely
> > +syntactic iff the defined behavior of the second access is unaffected
> > +by its dependency.
> 
> That's a very abstract way of describing the situation; it doesn't do a 
> good job of getting the real idea across.  It also mixes up two separate 
> ideas: behaviors being unaffected by a syntactic dependency and 
> behaviors being undefined.  They should be described separately. 

Many thanks for the feedback! I agree, the explanation works a lot
better once readers have been introduced to data, addr and ctrl
relations. 

> I would prefer something along these lines...

Shall I resubmit the patch with you as co-developer, or, given that it's
arguably your work now, would you like to submit the patch yourself?

Many thanks,
Paul

> ----------------------------------------
> 
> 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.
> 
> (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.  (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.
> 
> 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.
> 
> ----------------------------------------
> 
> Alan
> 
> > +Compilers are aware of syntactic dependencies and are within their
> > +rights to remove them as part of optimizations, thereby breaking any
> > +guarantees of ordering.
> > +
> > +Notable cases are dependencies eliminated through constant propagation
> > +or those where only one value leads to defined behavior as in the
> > +following example:
> > +
> > +	int a[1];
> > +	int i;
> > +
> > +	r1 = READ_ONCE(i);
> > +	r2 = READ_ONCE(a[r1]);
> > +
> > +The formal LKMM is unaware of syntactic dependencies and therefore
> > +predicts ordering.  However, since any other value than 0 for r1 would
> > +result in an out-of-bounds access, which is undefined behavior, r2 is
> > +not affected by its dependency to r1, making the above a purely
> > +syntactic dependency.
> > +
> >  Another issue arises from the fact that in C, arguments to many
> >  operators and function calls can be evaluated in any order.  For
> >  example:
> > -- 
> > 2.33.1
> >