GitHub-Mirror/Star64_linux
2
0
Fork 0
mirror of https://github.com/Fishwaldo/Star64_linux.git synced 2025-06-26 08:31:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

tools/memory-model: Rename link and rcu-path to rcu-link and rb

Browse source 
This patch makes a simple non-functional change to the RCU portion of
the Linux Kernel Memory Consistency Model by renaming the "link" and
"rcu-path" relations to "rcu-link" and "rb", respectively.

The name "link" was an unfortunate choice, because it was too generic
and subject to confusion with other meanings of the same word, which
occur quite often in LKMM documentation.  The name "rcu-path" is not
very appropriate, because the relation is analogous to the
happens-before (hb) and propagates-before (pb) relations -- although
that fact won't become apparent until the second patch in this series.

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Cc: Andrew Morton <akpm@linux-foundation.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Will Deacon <will.deacon@arm.com>
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: luc.maranget@inria.fr
Cc: npiggin@gmail.com
Link: http://lkml.kernel.org/r/1526340837-12222-1-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
This commit is contained in:
Alan Stern 2018-05-14 16:33:39 -07:00 • committed by Ingo Molnar
parent 1362ae43c5
commit 1ee2da5f9b
2 changed files with 53 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

89
tools/memory-model/Documentation/explanation.txt
View file

@ -27,7 +27,7 @@ Explanation of the Linux-Kernel Memory Consistency Model
19. AND THEN THERE WAS ALPHA 19. AND THEN THERE WAS ALPHA
20. THE HAPPENS-BEFORE RELATION: hb 20. THE HAPPENS-BEFORE RELATION: hb
21. THE PROPAGATES-BEFORE RELATION: pb 21. THE PROPAGATES-BEFORE RELATION: pb
22. RCU RELATIONS: link, gp-link, rscs-link, and rcu-path 22. RCU RELATIONS: rcu-link, gp-link, rscs-link, and rb
23. ODDS AND ENDS 23. ODDS AND ENDS
@ -1451,8 +1451,8 @@ they execute means that it cannot have cycles. This requirement is
the content of the LKMM's "propagation" axiom. the content of the LKMM's "propagation" axiom.
RCU RELATIONS: link, gp-link, rscs-link, and rcu-path RCU RELATIONS: rcu-link, gp-link, rscs-link, and rb
----------------------------------------------------- ---------------------------------------------------
RCU (Read-Copy-Update) is a powerful synchronization mechanism. It RCU (Read-Copy-Update) is a powerful synchronization mechanism. It
rests on two concepts: grace periods and read-side critical sections. rests on two concepts: grace periods and read-side critical sections.
@ -1509,8 +1509,8 @@ y, which occurs before the end of the critical section, did not
propagate to P1 before the end of the grace period, violating the propagate to P1 before the end of the grace period, violating the
Guarantee. Guarantee.
In the kernel's implementations of RCU, the business about stores In the kernel's implementations of RCU, the requirements for stores
propagating to every CPU is realized by placing strong fences at to propagate to every CPU are fulfilled by placing strong fences at
suitable places in the RCU-related code. Thus, if a critical section suitable places in the RCU-related code. Thus, if a critical section
starts before a grace period does then the critical section's CPU will starts before a grace period does then the critical section's CPU will
execute an smp_mb() fence after the end of the critical section and execute an smp_mb() fence after the end of the critical section and
@ -1523,19 +1523,19 @@ executes.
What exactly do we mean by saying that a critical section "starts What exactly do we mean by saying that a critical section "starts
before" or "ends after" a grace period? Some aspects of the meaning before" or "ends after" a grace period? Some aspects of the meaning
are pretty obvious, as in the example above, but the details aren't are pretty obvious, as in the example above, but the details aren't
entirely clear. The LKMM formalizes this notion by means of a entirely clear. The LKMM formalizes this notion by means of the
relation with the unfortunately generic name "link". It is a very rcu-link relation. rcu-link encompasses a very general notion of
general relation; among other things, X ->link Z includes cases where "before": Among other things, X ->rcu-link Z includes cases where X
X happens-before or is equal to some event Y which is equal to or happens-before or is equal to some event Y which is equal to or comes
comes before Z in the coherence order. Taking Y = Z, this says that before Z in the coherence order. When Y = Z this says that X ->rfe Z
X ->rfe Z implies X ->link Z, and taking Y = X, it says that X ->fr Z implies X ->rcu-link Z. In addition, when Y = X it says that X ->fr Z
and X ->co Z each imply X ->link Z. and X ->co Z each imply X ->rcu-link Z.
The formal definition of the link relation is more than a little The formal definition of the rcu-link relation is more than a little
obscure, and we won't give it here. It is closely related to the pb obscure, and we won't give it here. It is closely related to the pb
relation, and the details don't matter unless you want to comb through relation, and the details don't matter unless you want to comb through
a somewhat lengthy formal proof. Pretty much all you need to know a somewhat lengthy formal proof. Pretty much all you need to know
about link is the information in the preceding paragraph. about rcu-link is the information in the preceding paragraph.
The LKMM goes on to define the gp-link and rscs-link relations. They The LKMM goes on to define the gp-link and rscs-link relations. They
bring grace periods and read-side critical sections into the picture, bring grace periods and read-side critical sections into the picture,
@ -1543,32 +1543,33 @@ in the following way:
E ->gp-link F means there is a synchronize_rcu() fence event S E ->gp-link F means there is a synchronize_rcu() fence event S
and an event X such that E ->po S, either S ->po X or S = X, and an event X such that E ->po S, either S ->po X or S = X,
and X ->link F. In other words, E and F are connected by a and X ->rcu-link F. In other words, E and F are linked by a
grace period followed by an instance of link. grace period followed by an instance of rcu-link.
E ->rscs-link F means there is a critical section delimited by E ->rscs-link F means there is a critical section delimited by
an rcu_read_lock() fence L and an rcu_read_unlock() fence U, an rcu_read_lock() fence L and an rcu_read_unlock() fence U,
and an event X such that E ->po U, either L ->po X or L = X, and an event X such that E ->po U, either L ->po X or L = X,
and X ->link F. Roughly speaking, this says that some event and X ->rcu-link F. Roughly speaking, this says that some
in the same critical section as E is connected by link to F. event in the same critical section as E is linked by rcu-link
to F.
If we think of the link relation as standing for an extended "before", If we think of the rcu-link relation as standing for an extended
then E ->gp-link F says that E executes before a grace period which "before", then E ->gp-link F says that E executes before a grace
ends before F executes. (In fact it says more than this, because it period which ends before F executes. (In fact it covers more than
includes cases where E executes before a grace period and some store this, because it also includes cases where E executes before a grace
propagates to F's CPU before F executes and doesn't propagate to some period and some store propagates to F's CPU before F executes and
other CPU until after the grace period ends.) Similarly, doesn't propagate to some other CPU until after the grace period
E ->rscs-link F says that E is part of (or before the start of) a ends.) Similarly, E ->rscs-link F says that E is part of (or before
critical section which starts before F executes. the start of) a critical section which starts before F executes.
Putting this all together, the LKMM expresses the Grace Period Putting this all together, the LKMM expresses the Grace Period
Guarantee by requiring that there are no cycles consisting of gp-link Guarantee by requiring that there are no cycles consisting of gp-link
and rscs-link connections in which the number of gp-link instances is and rscs-link links in which the number of gp-link instances is >= the
>= the number of rscs-link instances. It does this by defining the number of rscs-link instances. It does this by defining the rb
rcu-path relation to link events E and F whenever it is possible to relation to link events E and F whenever it is possible to pass from E
pass from E to F by a sequence of gp-link and rscs-link connections to F by a sequence of gp-link and rscs-link links with at least as
with at least as many of the former as the latter. The LKMM's "rcu" many of the former as the latter. The LKMM's "rcu" axiom then says
axiom then says that there are no events E such that E ->rcu-path E. that there are no events E with E ->rb E.
Justifying this axiom takes some intellectual effort, but it is in Justifying this axiom takes some intellectual effort, but it is in
fact a valid formalization of the Grace Period Guarantee. We won't fact a valid formalization of the Grace Period Guarantee. We won't
@ -1585,10 +1586,10 @@ rcu_read_unlock() fence events delimiting the critical section in
question, and let S be the synchronize_rcu() fence event for the grace question, and let S be the synchronize_rcu() fence event for the grace
period. Saying that the critical section starts before S means there period. Saying that the critical section starts before S means there
are events E and F where E is po-after L (which marks the start of the are events E and F where E is po-after L (which marks the start of the
critical section), E is "before" F in the sense of the link relation, critical section), E is "before" F in the sense of the rcu-link
and F is po-before the grace period S: relation, and F is po-before the grace period S:
L ->po E ->link F ->po S. L ->po E ->rcu-link F ->po S.
Let W be the store mentioned above, let Z come before the end of the Let W be the store mentioned above, let Z come before the end of the
critical section and witness that W propagates to the critical critical section and witness that W propagates to the critical
@ -1600,12 +1601,12 @@ some event X which is po-after S. Symbolically, this amounts to:
The fr link from Y to W indicates that W has not propagated to Y's CPU The fr link from Y to W indicates that W has not propagated to Y's CPU
at the time that Y executes. From this, it can be shown (see the at the time that Y executes. From this, it can be shown (see the
discussion of the link relation earlier) that X and Z are connected by discussion of the rcu-link relation earlier) that X and Z are related
link, yielding: by rcu-link, yielding:
S ->po X ->link Z ->po U. S ->po X ->rcu-link Z ->po U.
These formulas say that S is po-between F and X, hence F ->gp-link Z The formulas say that S is po-between F and X, hence F ->gp-link Z
via X. They also say that Z comes before the end of the critical via X. They also say that Z comes before the end of the critical
section and E comes after its start, hence Z ->rscs-link F via E. But section and E comes after its start, hence Z ->rscs-link F via E. But
now we have a forbidden cycle: F ->gp-link Z ->rscs-link F. Thus the now we have a forbidden cycle: F ->gp-link Z ->rscs-link F. Thus the
@ -1635,13 +1636,13 @@ time with statement labels added to the memory access instructions:
} }
If r2 = 0 at the end then P0's store at X overwrites the value If r2 = 0 at the end then P0's store at X overwrites the value that
that P1's load at Z reads from, so we have Z ->fre X and thus P1's load at Z reads from, so we have Z ->fre X and thus Z ->rcu-link X.
Z ->link X. In addition, there is a synchronize_rcu() between Y and In addition, there is a synchronize_rcu() between Y and Z, so therefore
Z, so therefore we have Y ->gp-link X. we have Y ->gp-link X.
If r1 = 1 at the end then P1's load at Y reads from P0's store at W, If r1 = 1 at the end then P1's load at Y reads from P0's store at W,
so we have W ->link Y. In addition, W and X are in the same critical so we have W ->rcu-link Y. In addition, W and X are in the same critical
section, so therefore we have X ->rscs-link Y. section, so therefore we have X ->rscs-link Y.
This gives us a cycle, Y ->gp-link X ->rscs-link Y, with one gp-link This gives us a cycle, Y ->gp-link X ->rscs-link Y, with one gp-link

16
tools/memory-model/linux-kernel.cat
View file

@ -100,22 +100,22 @@ let rscs = po ; crit^-1 ; po?
* one but two non-rf relations, but only in conjunction with an RCU * one but two non-rf relations, but only in conjunction with an RCU
* read-side critical section. * read-side critical section.
*) *)
let link = hb* ; pb* ; prop let rcu-link = hb* ; pb* ; prop
(* Chains that affect the RCU grace-period guarantee *) (* Chains that affect the RCU grace-period guarantee *)
let gp-link = gp ; link let gp-link = gp ; rcu-link
let rscs-link = rscs ; link let rscs-link = rscs ; rcu-link
(* (*
* A cycle containing at least as many grace periods as RCU read-side * A cycle containing at least as many grace periods as RCU read-side
* critical sections is forbidden. * critical sections is forbidden.
*) *)
let rec rcu-path = let rec rb =
gp-link | gp-link |
(gp-link ; rscs-link) | (gp-link ; rscs-link) |
(rscs-link ; gp-link) | (rscs-link ; gp-link) |
(rcu-path ; rcu-path) | (rb ; rb) |
(gp-link ; rcu-path ; rscs-link) | (gp-link ; rb ; rscs-link) |
(rscs-link ; rcu-path ; gp-link) (rscs-link ; rb ; gp-link)
irreflexive rcu-path as rcu irreflexive rb as rcu