lkml.org 
[lkml]   [2022]   [Jan]   [25]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
Patch in this message
/
From
Subject[PATCH] tools/memory-model: Clarify syntactic and semantic dependencies
Date
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.

Link: https://lore.kernel.org/all/20211102190138.GA1497378@rowland.harvard.edu/
Signed-off-by: Paul Heidekrüger <paul.heidekrueger@in.tum.de>
Cc: Marco Elver <elver@google.com>
Cc: Charalampos Mainas <charalampos.mainas@gmail.com>
Cc: Pramod Bhatotia <pramod.bhatotia@in.tum.de>
---
.../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.
+
+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
\
 
 \ /
  Last update: 2022-01-25 18:42    [W:0.081 / U:0.628 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site