From: paulmck@kernel.org
To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
mingo@kernel.org
Cc: 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,
"Paul E . McKenney" <paulmck@kernel.org>
Subject: [PATCH tip/core/rcu 03/32] tools/memory-model/Documentation: Put redefinition of rcu-fence into explanation.txt
Date: Wed, 2 Oct 2019 17:26:21 -0700 [thread overview]
Message-ID: <20191003002650.11249-3-paulmck@kernel.org> (raw)
In-Reply-To: <20191003001039.GA8027@paulmck-ThinkPad-P72>
From: Alan Stern <stern@rowland.harvard.edu>
This patch updates the Linux Kernel Memory Model's explanation.txt
file to incorporate the introduction of the rcu-order relation and
the redefinition of rcu-fence made by commit 15aa25cbf0cc
("tools/memory-model: Change definition of rcu-fence").
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
tools/memory-model/Documentation/explanation.txt | 53 ++++++++++++++++--------
1 file changed, 36 insertions(+), 17 deletions(-)
diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index 1b52645..ecf6ccc 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/tools/memory-model/Documentation/explanation.txt
@@ -27,7 +27,7 @@ Explanation of the Linux-Kernel Memory Consistency Model
19. AND THEN THERE WAS ALPHA
20. THE HAPPENS-BEFORE RELATION: hb
21. THE PROPAGATES-BEFORE RELATION: pb
- 22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-fence, and rb
+ 22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb
23. LOCKING
24. ODDS AND ENDS
@@ -1425,8 +1425,8 @@ they execute means that it cannot have cycles. This requirement is
the content of the LKMM's "propagation" axiom.
-RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-fence, and rb
--------------------------------------------------------------
+RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb
+------------------------------------------------------------------------
RCU (Read-Copy-Update) is a powerful synchronization mechanism. It
rests on two concepts: grace periods and read-side critical sections.
@@ -1536,29 +1536,29 @@ Z's CPU before Z begins but doesn't propagate to some other CPU until
after X ends.) Similarly, X ->rcu-rscsi Y ->rcu-link Z says that X is
the end of a critical section which starts before Z begins.
-The LKMM goes on to define the rcu-fence relation as a sequence of
+The LKMM goes on to define the rcu-order relation as a sequence of
rcu-gp and rcu-rscsi links separated by rcu-link links, in which the
number of rcu-gp links is >= the number of rcu-rscsi links. For
example:
X ->rcu-gp Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V
-would imply that X ->rcu-fence V, because this sequence contains two
+would imply that X ->rcu-order V, because this sequence contains two
rcu-gp links and one rcu-rscsi link. (It also implies that
-X ->rcu-fence T and Z ->rcu-fence V.) On the other hand:
+X ->rcu-order T and Z ->rcu-order V.) On the other hand:
X ->rcu-rscsi Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V
-does not imply X ->rcu-fence V, because the sequence contains only
+does not imply X ->rcu-order V, because the sequence contains only
one rcu-gp link but two rcu-rscsi links.
-The rcu-fence relation is important because the Grace Period Guarantee
-means that rcu-fence acts kind of like a strong fence. In particular,
-E ->rcu-fence F implies not only that E begins before F ends, but also
-that any write po-before E will propagate to every CPU before any
-instruction po-after F can execute. (However, it does not imply that
-E must execute before F; in fact, each synchronize_rcu() fence event
-is linked to itself by rcu-fence as a degenerate case.)
+The rcu-order relation is important because the Grace Period Guarantee
+means that rcu-order links act kind of like strong fences. In
+particular, E ->rcu-order F implies not only that E begins before F
+ends, but also that any write po-before E will propagate to every CPU
+before any instruction po-after F can execute. (However, it does not
+imply that E must execute before F; in fact, each synchronize_rcu()
+fence event is linked to itself by rcu-order as a degenerate case.)
To prove this in full generality requires some intellectual effort.
We'll consider just a very simple case:
@@ -1585,7 +1585,26 @@ G's CPU before G starts must propagate to every CPU before C starts.
In particular, the write propagates to every CPU before F finishes
executing and hence before any instruction po-after F can execute.
This sort of reasoning can be extended to handle all the situations
-covered by rcu-fence.
+covered by rcu-order.
+
+The rcu-fence relation is a simple extension of rcu-order. While
+rcu-order only links certain fence events (calls to synchronize_rcu(),
+rcu_read_lock(), or rcu_read_unlock()), rcu-fence links any events
+that are separated by an rcu-order link. This is analogous to the way
+the strong-fence relation links events that are separated by an
+smp_mb() fence event (as mentioned above, rcu-order links act kind of
+like strong fences). Written symbolically, X ->rcu-fence Y means
+there are fence events E and F such that:
+
+ X ->po E ->rcu-order F ->po Y.
+
+From the discussion above, we see this implies not only that X
+executes before Y, but also (if X is a store) that X propagates to
+every CPU before Y executes. Thus rcu-fence is sort of a
+"super-strong" fence: Unlike the original strong fences (smp_mb() and
+synchronize_rcu()), rcu-fence is able to link events on different
+CPUs. (Perhaps this fact should lead us to say that rcu-fence isn't
+really a fence at all!)
Finally, the LKMM defines the RCU-before (rb) relation in terms of
rcu-fence. This is done in essentially the same way as the pb
@@ -1596,7 +1615,7 @@ before F, just as E ->pb F does (and for much the same reasons).
Putting this all together, the LKMM expresses the Grace Period
Guarantee by requiring that the rb relation does not contain a cycle.
Equivalently, this "rcu" axiom requires that there are no events E
-and F with E ->rcu-link F ->rcu-fence E. Or to put it a third way,
+and F with E ->rcu-link F ->rcu-order E. Or to put it a third way,
the axiom requires that there are no cycles consisting of rcu-gp and
rcu-rscsi alternating with rcu-link, where the number of rcu-gp links
is >= the number of rcu-rscsi links.
@@ -1750,7 +1769,7 @@ addition to normal RCU. The ideas involved are much the same as
above, with new relations srcu-gp and srcu-rscsi added to represent
SRCU grace periods and read-side critical sections. There is a
restriction on the srcu-gp and srcu-rscsi links that can appear in an
-rcu-fence sequence (the srcu-rscsi links must be paired with srcu-gp
+rcu-order sequence (the srcu-rscsi links must be paired with srcu-gp
links having the same SRCU domain with proper nesting); the details
are relatively unimportant.
--
2.9.5
next prev parent reply other threads:[~2019-10-03 0:28 UTC|newest]
Thread overview: 33+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-10-03 0:10 [PATCH memory-model 0/32] Memory-model updates Paul E. McKenney
2019-10-03 0:26 ` [PATCH tip/core/rcu 01/32] tools/memory-model: Fix data race detection for unordered store and load paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 02/32] tools/memory-model/Documentation: Fix typos in explanation.txt paulmck
2019-10-03 0:26 ` paulmck [this message]
2019-10-03 0:26 ` [PATCH tip/core/rcu 04/32] tools/memory-model/Documentation: Add plain accesses and data races to explanation.txt paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 05/32] tools/memory-model: Make judgelitmus.sh note timeouts paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 06/32] tools/memory-model: Make cmplitmushist.sh " paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 07/32] tools/memory-model: Make judgelitmus.sh identify bad macros paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 08/32] tools/memory-model: Make judgelitmus.sh detect hard deadlocks paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 09/32] tools/memory-model: Fix paulmck email address on pre-existing scripts paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 10/32] tools/memory-model: Update parseargs.sh for hardware verification paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 11/32] tools/memory-model: Make judgelitmus.sh handle hardware verifications paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 12/32] tools/memory-model: Add simpletest.sh to check locking, RCU, and SRCU paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 13/32] tools/memory-model: Fix checkalllitmus.sh comment paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 14/32] tools/memory-model: Hardware checking for check{,all}litmus.sh paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 15/32] tools/memory-model: Make judgelitmus.sh ransack .litmus.out files paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 16/32] tools/memory-model: Split runlitmus.sh out of checklitmus.sh paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 17/32] tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 18/32] tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 19/32] tools/memory-model: Keep assembly-language litmus tests paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 20/32] tools/memory-model: Allow herd to deduce CPU type paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 21/32] tools/memory-model: Make runlitmus.sh check for jingle errors paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 22/32] tools/memory-model: Add -v flag to jingle7 runs paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 23/32] tools/memory-model: Implement --hw support for checkghlitmus.sh paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 24/32] tools/memory-model: Fix scripting --jobs argument paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 25/32] tools/memory-model: Make checkghlitmus.sh use mselect7 paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 26/32] tools/memory-model: Make history-check scripts " paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 27/32] tools/memory-model: Add "--" to parseargs.sh for additional arguments paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 28/32] tools/memory-model: Repair parseargs.sh header comment paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 29/32] tools/memory-model: Add checktheselitmus.sh to run specified litmus tests paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 30/32] tools/memory-model: Add data-race capabilities to judgelitmus.sh paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 31/32] tools/memory-model: Make judgelitmus.sh handle scripted Result: tag paulmck
2019-10-03 0:26 ` [PATCH tip/core/rcu 32/32] tools/memory-model: Use "-unroll 0" to keep --hw runs finite paulmck
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=20191003002650.11249-3-paulmck@kernel.org \
--to=paulmck@kernel.org \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=j.alglave@ucl.ac.uk \
--cc=linux-arch@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=mingo@kernel.org \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--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;
as well as URLs for NNTP newsgroup(s).