From: Marco Elver <elver@google.com>
To: elver@google.com
Cc: paulmck@kernel.org, andreyknvl@google.com, glider@google.com,
dvyukov@google.com, kasan-dev@googlegroups.com,
linux-kernel@vger.kernel.org, stern@rowland.harvard.edu,
parri.andrea@gmail.com, will@kernel.org, peterz@infradead.org,
boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com,
j.alglave@ucl.ac.uk, luc.maranget@inria.fr, akiyks@gmail.com,
dlustig@nvidia.com, joel@joelfernandes.org,
linux-arch@vger.kernel.org
Subject: [PATCH] tools/memory-model/Documentation: Fix "conflict" definition
Date: Fri, 28 Feb 2020 17:46:21 +0100 [thread overview]
Message-ID: <20200228164621.87523-1-elver@google.com> (raw)
For language-level memory consistency models that are adaptations of
data-race-free, the definition of "data race" can be summarized as
"concurrent conflicting accesses, where at least one is non-sync/plain".
The definition of "conflict" should not include the type of access nor
whether the accesses are concurrent or not, which this patch addresses
for explanation.txt.
The definition of "data race" remains unchanged, but the informal
definition for "conflict" is restored to what can be found in the
literature.
Signed-by: Marco Elver <elver@google.com>
---
tools/memory-model/Documentation/explanation.txt | 15 ++++++---------
1 file changed, 6 insertions(+), 9 deletions(-)
diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index e91a2eb19592a..11cf89b5b85d9 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/tools/memory-model/Documentation/explanation.txt
@@ -1986,18 +1986,15 @@ violates the compiler's assumptions, which would render the ultimate
outcome undefined.
In technical terms, the compiler is allowed to assume that when the
-program executes, there will not be any data races. A "data race"
-occurs when two conflicting memory accesses execute concurrently;
-two memory accesses "conflict" if:
+program executes, there will not be any data races. A "data race"
+occurs if:
- they access the same location,
+ two concurrent memory accesses "conflict";
- they occur on different CPUs (or in different threads on the
- same CPU),
+ and at least one of the accesses is a plain access;
- at least one of them is a plain access,
-
- and at least one of them is a store.
+ where two memory accesses "conflict" if they access the same
+ memory location, and at least one performs a write;
The LKMM tries to determine whether a program contains two conflicting
accesses which may execute concurrently; if it does then the LKMM says
--
2.25.1.481.gfbce0eb801-goog
next reply other threads:[~2020-02-28 16:47 UTC|newest]
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
2020-02-28 16:46 Marco Elver [this message]
2020-02-28 17:24 ` [PATCH] tools/memory-model/Documentation: Fix "conflict" definition Alan Stern
2020-02-28 18:54 ` Marco Elver
2020-02-28 19:00 ` Marco Elver
2020-02-28 20:20 ` Alan Stern
2020-02-28 20:31 ` Marco Elver
2020-03-02 14:21 ` Marco Elver
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20200228164621.87523-1-elver@google.com \
--to=elver@google.com \
--cc=akiyks@gmail.com \
--cc=andreyknvl@google.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=dvyukov@google.com \
--cc=glider@google.com \
--cc=j.alglave@ucl.ac.uk \
--cc=joel@joelfernandes.org \
--cc=kasan-dev@googlegroups.com \
--cc=linux-arch@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--cc=paulmck@kernel.org \
--cc=peterz@infradead.org \
--cc=stern@rowland.harvard.edu \
--cc=will@kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox