[PATCH memory-model 02/19] tools/memory-model: Redefine rb in terms of rcu-fence

[Paul E. McKenney]

From: Alan Stern 

This patch reorganizes the definition of rb in the Linux Kernel Memory
Consistency Model.  The relation is now expressed in terms of
rcu-fence, which consists of a sequence of gp and rscs links separated
by rcu-link links, in which the number of occurrences of gp is >= the
number of occurrences of rscs.

Arguments similar to those published in
http://diy.inria.fr/linux/long.pdf show that rcu-fence behaves like an
inter-CPU strong fence.  Furthermore, the definition of rb in terms of
rcu-fence is highly analogous to the definition of pb in terms of
strong-fence, which can help explain why rcu-path expresses a form of
temporal ordering.

This change should not affect the semantics of the memory model, just
its internal organization.

Signed-off-by: Alan Stern 
Reviewed-by: Boqun Feng 
Reviewed-by: Andrea Parri 
Signed-off-by: Paul E. McKenney 
---
 tools/memory-model/Documentation/explanation.txt | 168 +++
 tools/memory-model/linux-kernel.cat  |  33 +++--
 2 files changed, 129 insertions(+), 72 deletions(-)

diff --git a/tools/memory-model/Documentation/explanation.txt 
b/tools/memory-model/Documentation/explanation.txt
index 1a387d703212..1b09f3175a1f 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, gp-link, rscs-link, and rb
+  22. RCU RELATIONS: rcu-link, gp, rscs, rcu-fence, and rb
   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.
 
 
-RCU RELATIONS: rcu-link, gp-link, rscs-link, and rb

+RCU RELATIONS: rcu-link, gp, rscs, 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.
@@ -1537,49 +1537,100 @@ 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
 about rcu-link is the information in the preceding paragraph.
 
-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,
-in the following way:
+The LKMM also defines the gp and rscs relations.  They bring grace
+periods and read-side critical sections into the picture, in the
+following way:
 
-   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 X ->rcu-link F.  In other words, E and F are linked by a
-   grace period followed by an instance of rcu-link.
+   E ->gp F means there is a synchronize_rcu() fence event S such
+   that E ->po S and either S ->po F or S = F.  In simple terms,
+   there is a grace period po-between E and F.
 
-   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,
-   and an event X such that E ->po U, either L ->po X or L = X,
-   and X ->rcu-link F.  Roughly speaking, this says that some
-   event in the same critical section as E is linked by rcu-link
-   to F.
+   E ->rscs F means there is a critical section delimited by an
+   rcu_read_lock() fence L and an rcu_read_unlock() fence U, such
+   that E ->po U and either L ->po F or L = F.  You can think of
+   this as saying that E and F are in the same critical section
+   (in fact, it also allows E to be po-before the start of the
+   critical section and F to be po-after the end).
 
 If we think of the rcu-link relation as standing for an extended
-"before", then E ->gp-link F says that E executes before a grace
-period which ends before F executes.  (In fact it covers more than
-this, because it also includes cases where E executes before a grace
-period and some store propagates to F's CPU before F executes and
-doesn't propagate to some other CPU until after the grace period
-ends.)  Similarly, E ->rscs-link F says that E is part of (or before
-the start of) a critical section which starts before F executes.
+"before", then X ->gp Y ->rcu-link Z says that X executes before a
+grace period which ends before Z executes.  (In fact it covers more
+than this, because it also includes cases where X executes before a
+grace period and some store propagates to Z's CPU before Z executes
+but doesn't propagate to some other CPU until after the grace period
+ends.)  Similarly, X ->rscs Y ->rcu-link Z 

[PATCH memory-model 02/19] tools/memory-model: Redefine rb in terms of rcu-fence

[Paul E. McKenney]

From: Alan Stern 

This patch reorganizes the definition of rb in the Linux Kernel Memory
Consistency Model.  The relation is now expressed in terms of
rcu-fence, which consists of a sequence of gp and rscs links separated
by rcu-link links, in which the number of occurrences of gp is >= the
number of occurrences of rscs.

Arguments similar to those published in
http://diy.inria.fr/linux/long.pdf show that rcu-fence behaves like an
inter-CPU strong fence.  Furthermore, the definition of rb in terms of
rcu-fence is highly analogous to the definition of pb in terms of
strong-fence, which can help explain why rcu-path expresses a form of
temporal ordering.

This change should not affect the semantics of the memory model, just
its internal organization.

Signed-off-by: Alan Stern 
Reviewed-by: Boqun Feng 
Reviewed-by: Andrea Parri 
Signed-off-by: Paul E. McKenney 
---
 tools/memory-model/Documentation/explanation.txt | 168 +++
 tools/memory-model/linux-kernel.cat  |  33 +++--
 2 files changed, 129 insertions(+), 72 deletions(-)

diff --git a/tools/memory-model/Documentation/explanation.txt 
b/tools/memory-model/Documentation/explanation.txt
index 1a387d703212..1b09f3175a1f 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, gp-link, rscs-link, and rb
+  22. RCU RELATIONS: rcu-link, gp, rscs, rcu-fence, and rb
   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.
 
 
-RCU RELATIONS: rcu-link, gp-link, rscs-link, and rb

+RCU RELATIONS: rcu-link, gp, rscs, 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.
@@ -1537,49 +1537,100 @@ 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
 about rcu-link is the information in the preceding paragraph.
 
-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,
-in the following way:
+The LKMM also defines the gp and rscs relations.  They bring grace
+periods and read-side critical sections into the picture, in the
+following way:
 
-   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 X ->rcu-link F.  In other words, E and F are linked by a
-   grace period followed by an instance of rcu-link.
+   E ->gp F means there is a synchronize_rcu() fence event S such
+   that E ->po S and either S ->po F or S = F.  In simple terms,
+   there is a grace period po-between E and F.
 
-   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,
-   and an event X such that E ->po U, either L ->po X or L = X,
-   and X ->rcu-link F.  Roughly speaking, this says that some
-   event in the same critical section as E is linked by rcu-link
-   to F.
+   E ->rscs F means there is a critical section delimited by an
+   rcu_read_lock() fence L and an rcu_read_unlock() fence U, such
+   that E ->po U and either L ->po F or L = F.  You can think of
+   this as saying that E and F are in the same critical section
+   (in fact, it also allows E to be po-before the start of the
+   critical section and F to be po-after the end).
 
 If we think of the rcu-link relation as standing for an extended
-"before", then E ->gp-link F says that E executes before a grace
-period which ends before F executes.  (In fact it covers more than
-this, because it also includes cases where E executes before a grace
-period and some store propagates to F's CPU before F executes and
-doesn't propagate to some other CPU until after the grace period
-ends.)  Similarly, E ->rscs-link F says that E is part of (or before
-the start of) a critical section which starts before F executes.
+"before", then X ->gp Y ->rcu-link Z says that X executes before a
+grace period which ends before Z executes.  (In fact it covers more
+than this, because it also includes cases where X executes before a
+grace period and some store propagates to Z's CPU before Z executes
+but doesn't propagate to some other CPU until after the grace period
+ends.)  Similarly, X ->rscs Y ->rcu-link Z says that X is part of (or
+before the start of) a critical section which starts before Z
+executes.
+
+The LKMM goes on to