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 > >
